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
Structured
Syntax definition
cif
Description:
Extend class notation to include the conditional operator for classes.
Ref
Expression
Assertion
cif
class
if (
𝜑
,
𝐴
,
𝐵
)