Metamath Proof Explorer


Theorem dfif3

Description: Alternate definition of the conditional operator df-if . Note that ph is independent of x i.e. a constant true or false. (Contributed by NM, 25-Aug-2013) (Revised by Mario Carneiro, 8-Sep-2013)

Ref Expression
Hypothesis dfif3.1 C=x|φ
Assertion dfif3 ifφAB=ACBVC

Proof

Step Hyp Ref Expression
1 dfif3.1 C=x|φ
2 dfif6 ifφAB=yA|φyB|¬φ
3 biidd x=yφφ
4 3 cbvabv x|φ=y|φ
5 1 4 eqtri C=y|φ
6 5 ineq2i AC=Ay|φ
7 dfrab3 yA|φ=Ay|φ
8 6 7 eqtr4i AC=yA|φ
9 dfrab3 yB|¬φ=By|¬φ
10 biidd y=zφφ
11 10 notabw y|¬φ=Vz|φ
12 biidd x=zφφ
13 12 cbvabv x|φ=z|φ
14 1 13 eqtri C=z|φ
15 14 difeq2i VC=Vz|φ
16 11 15 eqtr4i y|¬φ=VC
17 16 ineq2i By|¬φ=BVC
18 9 17 eqtr2i BVC=yB|¬φ
19 8 18 uneq12i ACBVC=yA|φyB|¬φ
20 2 19 eqtr4i ifφAB=ACBVC