Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
The conditional operator for classes
iftruei
Next ⟩
iftrued
Metamath Proof Explorer
Ascii
Unicode
Theorem
iftruei
Description:
Inference associated with
iftrue
.
(Contributed by
BJ
, 7-Oct-2018)
Ref
Expression
Hypothesis
iftruei.1
⊢
φ
Assertion
iftruei
⊢
if
φ
A
B
=
A
Proof
Step
Hyp
Ref
Expression
1
iftruei.1
⊢
φ
2
iftrue
⊢
φ
→
if
φ
A
B
=
A
3
1
2
ax-mp
⊢
if
φ
A
B
=
A