:: deftheorem Def8 defines WFF ZF_LANG:def 8 :
for b₁ being non empty set holds
( b₁ = WFF iff ( ( for a being set st a in b₁ holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in b₁ & x 'in' y in b₁ ) ) & ( for p being FinSequence of NAT st p in b₁ holds
'not' p in b₁ ) & ( for p, q being FinSequence of NAT st p in b₁ & q in b₁ holds
p '&' q in b₁ ) & ( for x being Variable
for p being FinSequence of NAT st p in b₁ holds
All (x,p) in b₁ ) & ( for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds
'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p '&' q in D ) & ( for x being Variable
for p being FinSequence of NAT st p in D holds
All (x,p) in D ) holds
b₁ c= D ) ) );