Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
The conditional operator for classes
cif
Next ⟩
df-if
Metamath Proof Explorer
Ascii
Unicode
Syntax definition
cif
Description:
Extend class notation to include the conditional operator for classes.
Ref
Expression
Assertion
cif
$${class}if\left({\phi},{A},{B}\right)$$