MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfif5 Structured version   Visualization version   GIF version

Theorem dfif5 4079
Description: Alternate definition of the conditional operator df-if 4064. Note that 𝜑 is independent of 𝑥 i.e. a constant true or false (see also ab0orv 3932). (Contributed by Gérard Lang, 18-Aug-2013.)
Hypothesis
Ref Expression
dfif3.1 𝐶 = {𝑥𝜑}
Assertion
Ref Expression
dfif5 if(𝜑, 𝐴, 𝐵) = ((𝐴𝐵) ∪ (((𝐴𝐵) ∩ 𝐶) ∪ ((𝐵𝐴) ∩ (V ∖ 𝐶))))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐶(𝑥)

Proof of Theorem dfif5
StepHypRef Expression
1 inindi 3813 . 2 ((𝐴𝐵) ∩ ((𝐴 ∪ (V ∖ 𝐶)) ∩ (𝐵𝐶))) = (((𝐴𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶))) ∩ ((𝐴𝐵) ∩ (𝐵𝐶)))
2 dfif3.1 . . 3 𝐶 = {𝑥𝜑}
32dfif4 4078 . 2 if(𝜑, 𝐴, 𝐵) = ((𝐴𝐵) ∩ ((𝐴 ∪ (V ∖ 𝐶)) ∩ (𝐵𝐶)))
4 undir 3857 . . 3 ((𝐴𝐵) ∪ (((𝐴𝐵) ∩ 𝐶) ∪ ((𝐵𝐴) ∩ (V ∖ 𝐶)))) = ((𝐴 ∪ (((𝐴𝐵) ∩ 𝐶) ∪ ((𝐵𝐴) ∩ (V ∖ 𝐶)))) ∩ (𝐵 ∪ (((𝐴𝐵) ∩ 𝐶) ∪ ((𝐵𝐴) ∩ (V ∖ 𝐶)))))
5 unidm 3739 . . . . . . . 8 (𝐴𝐴) = 𝐴
65uneq1i 3746 . . . . . . 7 ((𝐴𝐴) ∪ (𝐵 ∩ (V ∖ 𝐶))) = (𝐴 ∪ (𝐵 ∩ (V ∖ 𝐶)))
7 unass 3753 . . . . . . 7 ((𝐴𝐴) ∪ (𝐵 ∩ (V ∖ 𝐶))) = (𝐴 ∪ (𝐴 ∪ (𝐵 ∩ (V ∖ 𝐶))))
8 undi 3855 . . . . . . 7 (𝐴 ∪ (𝐵 ∩ (V ∖ 𝐶))) = ((𝐴𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶)))
96, 7, 83eqtr3ri 2652 . . . . . 6 ((𝐴𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶))) = (𝐴 ∪ (𝐴 ∪ (𝐵 ∩ (V ∖ 𝐶))))
10 undi 3855 . . . . . . . 8 (𝐴 ∪ ((𝐴𝐵) ∩ 𝐶)) = ((𝐴 ∪ (𝐴𝐵)) ∩ (𝐴𝐶))
11 undifabs 4022 . . . . . . . . 9 (𝐴 ∪ (𝐴𝐵)) = 𝐴
1211ineq1i 3793 . . . . . . . 8 ((𝐴 ∪ (𝐴𝐵)) ∩ (𝐴𝐶)) = (𝐴 ∩ (𝐴𝐶))
13 inabs 3838 . . . . . . . 8 (𝐴 ∩ (𝐴𝐶)) = 𝐴
1410, 12, 133eqtri 2647 . . . . . . 7 (𝐴 ∪ ((𝐴𝐵) ∩ 𝐶)) = 𝐴
15 undif2 4021 . . . . . . . . 9 (𝐴 ∪ (𝐵𝐴)) = (𝐴𝐵)
1615ineq1i 3793 . . . . . . . 8 ((𝐴 ∪ (𝐵𝐴)) ∩ (𝐴 ∪ (V ∖ 𝐶))) = ((𝐴𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶)))
17 undi 3855 . . . . . . . 8 (𝐴 ∪ ((𝐵𝐴) ∩ (V ∖ 𝐶))) = ((𝐴 ∪ (𝐵𝐴)) ∩ (𝐴 ∪ (V ∖ 𝐶)))
1816, 17, 83eqtr4i 2653 . . . . . . 7 (𝐴 ∪ ((𝐵𝐴) ∩ (V ∖ 𝐶))) = (𝐴 ∪ (𝐵 ∩ (V ∖ 𝐶)))
1914, 18uneq12i 3748 . . . . . 6 ((𝐴 ∪ ((𝐴𝐵) ∩ 𝐶)) ∪ (𝐴 ∪ ((𝐵𝐴) ∩ (V ∖ 𝐶)))) = (𝐴 ∪ (𝐴 ∪ (𝐵 ∩ (V ∖ 𝐶))))
209, 19eqtr4i 2646 . . . . 5 ((𝐴𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶))) = ((𝐴 ∪ ((𝐴𝐵) ∩ 𝐶)) ∪ (𝐴 ∪ ((𝐵𝐴) ∩ (V ∖ 𝐶))))
21 unundi 3757 . . . . 5 (𝐴 ∪ (((𝐴𝐵) ∩ 𝐶) ∪ ((𝐵𝐴) ∩ (V ∖ 𝐶)))) = ((𝐴 ∪ ((𝐴𝐵) ∩ 𝐶)) ∪ (𝐴 ∪ ((𝐵𝐴) ∩ (V ∖ 𝐶))))
2220, 21eqtr4i 2646 . . . 4 ((𝐴𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶))) = (𝐴 ∪ (((𝐴𝐵) ∩ 𝐶) ∪ ((𝐵𝐴) ∩ (V ∖ 𝐶))))
23 unass 3753 . . . . . 6 (((𝐴𝐶) ∪ 𝐵) ∪ 𝐵) = ((𝐴𝐶) ∪ (𝐵𝐵))
24 undi 3855 . . . . . . . . 9 (𝐵 ∪ (𝐴𝐶)) = ((𝐵𝐴) ∩ (𝐵𝐶))
25 uncom 3740 . . . . . . . . 9 ((𝐴𝐶) ∪ 𝐵) = (𝐵 ∪ (𝐴𝐶))
26 undif2 4021 . . . . . . . . . 10 (𝐵 ∪ (𝐴𝐵)) = (𝐵𝐴)
2726ineq1i 3793 . . . . . . . . 9 ((𝐵 ∪ (𝐴𝐵)) ∩ (𝐵𝐶)) = ((𝐵𝐴) ∩ (𝐵𝐶))
2824, 25, 273eqtr4i 2653 . . . . . . . 8 ((𝐴𝐶) ∪ 𝐵) = ((𝐵 ∪ (𝐴𝐵)) ∩ (𝐵𝐶))
29 undi 3855 . . . . . . . 8 (𝐵 ∪ ((𝐴𝐵) ∩ 𝐶)) = ((𝐵 ∪ (𝐴𝐵)) ∩ (𝐵𝐶))
3028, 29eqtr4i 2646 . . . . . . 7 ((𝐴𝐶) ∪ 𝐵) = (𝐵 ∪ ((𝐴𝐵) ∩ 𝐶))
31 undi 3855 . . . . . . . 8 (𝐵 ∪ ((𝐵𝐴) ∩ (V ∖ 𝐶))) = ((𝐵 ∪ (𝐵𝐴)) ∩ (𝐵 ∪ (V ∖ 𝐶)))
32 undifabs 4022 . . . . . . . . 9 (𝐵 ∪ (𝐵𝐴)) = 𝐵
3332ineq1i 3793 . . . . . . . 8 ((𝐵 ∪ (𝐵𝐴)) ∩ (𝐵 ∪ (V ∖ 𝐶))) = (𝐵 ∩ (𝐵 ∪ (V ∖ 𝐶)))
34 inabs 3838 . . . . . . . 8 (𝐵 ∩ (𝐵 ∪ (V ∖ 𝐶))) = 𝐵
3531, 33, 343eqtrri 2648 . . . . . . 7 𝐵 = (𝐵 ∪ ((𝐵𝐴) ∩ (V ∖ 𝐶)))
3630, 35uneq12i 3748 . . . . . 6 (((𝐴𝐶) ∪ 𝐵) ∪ 𝐵) = ((𝐵 ∪ ((𝐴𝐵) ∩ 𝐶)) ∪ (𝐵 ∪ ((𝐵𝐴) ∩ (V ∖ 𝐶))))
37 unidm 3739 . . . . . . 7 (𝐵𝐵) = 𝐵
3837uneq2i 3747 . . . . . 6 ((𝐴𝐶) ∪ (𝐵𝐵)) = ((𝐴𝐶) ∪ 𝐵)
3923, 36, 383eqtr3ri 2652 . . . . 5 ((𝐴𝐶) ∪ 𝐵) = ((𝐵 ∪ ((𝐴𝐵) ∩ 𝐶)) ∪ (𝐵 ∪ ((𝐵𝐴) ∩ (V ∖ 𝐶))))
40 uncom 3740 . . . . . . 7 (𝐵𝐶) = (𝐶𝐵)
4140ineq2i 3794 . . . . . 6 ((𝐴𝐵) ∩ (𝐵𝐶)) = ((𝐴𝐵) ∩ (𝐶𝐵))
42 undir 3857 . . . . . 6 ((𝐴𝐶) ∪ 𝐵) = ((𝐴𝐵) ∩ (𝐶𝐵))
4341, 42eqtr4i 2646 . . . . 5 ((𝐴𝐵) ∩ (𝐵𝐶)) = ((𝐴𝐶) ∪ 𝐵)
44 unundi 3757 . . . . 5 (𝐵 ∪ (((𝐴𝐵) ∩ 𝐶) ∪ ((𝐵𝐴) ∩ (V ∖ 𝐶)))) = ((𝐵 ∪ ((𝐴𝐵) ∩ 𝐶)) ∪ (𝐵 ∪ ((𝐵𝐴) ∩ (V ∖ 𝐶))))
4539, 43, 443eqtr4i 2653 . . . 4 ((𝐴𝐵) ∩ (𝐵𝐶)) = (𝐵 ∪ (((𝐴𝐵) ∩ 𝐶) ∪ ((𝐵𝐴) ∩ (V ∖ 𝐶))))
4622, 45ineq12i 3795 . . 3 (((𝐴𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶))) ∩ ((𝐴𝐵) ∩ (𝐵𝐶))) = ((𝐴 ∪ (((𝐴𝐵) ∩ 𝐶) ∪ ((𝐵𝐴) ∩ (V ∖ 𝐶)))) ∩ (𝐵 ∪ (((𝐴𝐵) ∩ 𝐶) ∪ ((𝐵𝐴) ∩ (V ∖ 𝐶)))))
474, 46eqtr4i 2646 . 2 ((𝐴𝐵) ∪ (((𝐴𝐵) ∩ 𝐶) ∪ ((𝐵𝐴) ∩ (V ∖ 𝐶)))) = (((𝐴𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶))) ∩ ((𝐴𝐵) ∩ (𝐵𝐶)))
481, 3, 473eqtr4i 2653 1 if(𝜑, 𝐴, 𝐵) = ((𝐴𝐵) ∪ (((𝐴𝐵) ∩ 𝐶) ∪ ((𝐵𝐴) ∩ (V ∖ 𝐶))))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1480  {cab 2607  Vcvv 3189  cdif 3556  cun 3557  cin 3558  ifcif 4063
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rab 2916  df-v 3191  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator