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
Ascii
Unicode
Syntax definition
wnfc
Description:
Extend wff definition to include the not-free predicate for classes.
Ref
Expression
Assertion
wnfc
$${wff}\underset{\_}{\u2132}{x}\phantom{\rule{.4em}{0ex}}{A}$$