Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
Class form not-free predicate
wnfc
Next ⟩
nfcjust
Metamath Proof Explorer
Unicode
Structured
Syntax definition
wnfc
Description:
Extend wff definition to include the not-free predicate for classes.
Ref
Expression
Assertion
wnfc
wff F/_ x A