MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfif5 Structured version   Visualization version   GIF version
Theorem dfif5 4545
Description: Alternate definition of the conditional operator df-if 4530. Note that πœ‘ is independent of π‘₯ i.e. a constant true or false (see also ab0orv 4379). (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 4227 . 2 ((𝐴 βˆͺ 𝐡) ∩ ((𝐴 βˆͺ (V βˆ– 𝐢)) ∩ (𝐡 βˆͺ 𝐢))) = (((𝐴 βˆͺ 𝐡) ∩ (𝐴 βˆͺ (V βˆ– 𝐢))) ∩ ((𝐴 βˆͺ 𝐡) ∩ (𝐡 βˆͺ 𝐢)))
2 dfif3.1 . . 3 𝐢 = {π‘₯ ∣ πœ‘}
32dfif4 4544 . 2 if(πœ‘, 𝐴, 𝐡) = ((𝐴 βˆͺ 𝐡) ∩ ((𝐴 βˆͺ (V βˆ– 𝐢)) ∩ (𝐡 βˆͺ 𝐢)))
4 undir 4277 . . 3 ((𝐴 ∩ 𝐡) βˆͺ (((𝐴 βˆ– 𝐡) ∩ 𝐢) βˆͺ ((𝐡 βˆ– 𝐴) ∩ (V βˆ– 𝐢)))) = ((𝐴 βˆͺ (((𝐴 βˆ– 𝐡) ∩ 𝐢) βˆͺ ((𝐡 βˆ– 𝐴) ∩ (V βˆ– 𝐢)))) ∩ (𝐡 βˆͺ (((𝐴 βˆ– 𝐡) ∩ 𝐢) βˆͺ ((𝐡 βˆ– 𝐴) ∩ (V βˆ– 𝐢)))))
5 unidm 4153 . . . . . . . 8 (𝐴 βˆͺ 𝐴) = 𝐴
65uneq1i 4160 . . . . . . 7 ((𝐴 βˆͺ 𝐴) βˆͺ (𝐡 ∩ (V βˆ– 𝐢))) = (𝐴 βˆͺ (𝐡 ∩ (V βˆ– 𝐢)))
7 unass 4167 . . . . . . 7 ((𝐴 βˆͺ 𝐴) βˆͺ (𝐡 ∩ (V βˆ– 𝐢))) = (𝐴 βˆͺ (𝐴 βˆͺ (𝐡 ∩ (V βˆ– 𝐢))))
8 undi 4275 . . . . . . 7 (𝐴 βˆͺ (𝐡 ∩ (V βˆ– 𝐢))) = ((𝐴 βˆͺ 𝐡) ∩ (𝐴 βˆͺ (V βˆ– 𝐢)))
96, 7, 83eqtr3ri 2767 . . . . . 6 ((𝐴 βˆͺ 𝐡) ∩ (𝐴 βˆͺ (V βˆ– 𝐢))) = (𝐴 βˆͺ (𝐴 βˆͺ (𝐡 ∩ (V βˆ– 𝐢))))
10 undi 4275 . . . . . . . 8 (𝐴 βˆͺ ((𝐴 βˆ– 𝐡) ∩ 𝐢)) = ((𝐴 βˆͺ (𝐴 βˆ– 𝐡)) ∩ (𝐴 βˆͺ 𝐢))
11 undifabs 4478 . . . . . . . . 9 (𝐴 βˆͺ (𝐴 βˆ– 𝐡)) = 𝐴
1211ineq1i 4209 . . . . . . . 8 ((𝐴 βˆͺ (𝐴 βˆ– 𝐡)) ∩ (𝐴 βˆͺ 𝐢)) = (𝐴 ∩ (𝐴 βˆͺ 𝐢))
13 inabs 4256 . . . . . . . 8 (𝐴 ∩ (𝐴 βˆͺ 𝐢)) = 𝐴
1410, 12, 133eqtri 2762 . . . . . . 7 (𝐴 βˆͺ ((𝐴 βˆ– 𝐡) ∩ 𝐢)) = 𝐴
15 undif2 4477 . . . . . . . . 9 (𝐴 βˆͺ (𝐡 βˆ– 𝐴)) = (𝐴 βˆͺ 𝐡)
1615ineq1i 4209 . . . . . . . 8 ((𝐴 βˆͺ (𝐡 βˆ– 𝐴)) ∩ (𝐴 βˆͺ (V βˆ– 𝐢))) = ((𝐴 βˆͺ 𝐡) ∩ (𝐴 βˆͺ (V βˆ– 𝐢)))
17 undi 4275 . . . . . . . 8 (𝐴 βˆͺ ((𝐡 βˆ– 𝐴) ∩ (V βˆ– 𝐢))) = ((𝐴 βˆͺ (𝐡 βˆ– 𝐴)) ∩ (𝐴 βˆͺ (V βˆ– 𝐢)))
1816, 17, 83eqtr4i 2768 . . . . . . 7 (𝐴 βˆͺ ((𝐡 βˆ– 𝐴) ∩ (V βˆ– 𝐢))) = (𝐴 βˆͺ (𝐡 ∩ (V βˆ– 𝐢)))
1914, 18uneq12i 4162 . . . . . 6 ((𝐴 βˆͺ ((𝐴 βˆ– 𝐡) ∩ 𝐢)) βˆͺ (𝐴 βˆͺ ((𝐡 βˆ– 𝐴) ∩ (V βˆ– 𝐢)))) = (𝐴 βˆͺ (𝐴 βˆͺ (𝐡 ∩ (V βˆ– 𝐢))))
209, 19eqtr4i 2761 . . . . 5 ((𝐴 βˆͺ 𝐡) ∩ (𝐴 βˆͺ (V βˆ– 𝐢))) = ((𝐴 βˆͺ ((𝐴 βˆ– 𝐡) ∩ 𝐢)) βˆͺ (𝐴 βˆͺ ((𝐡 βˆ– 𝐴) ∩ (V βˆ– 𝐢))))
21 unundi 4171 . . . . 5 (𝐴 βˆͺ (((𝐴 βˆ– 𝐡) ∩ 𝐢) βˆͺ ((𝐡 βˆ– 𝐴) ∩ (V βˆ– 𝐢)))) = ((𝐴 βˆͺ ((𝐴 βˆ– 𝐡) ∩ 𝐢)) βˆͺ (𝐴 βˆͺ ((𝐡 βˆ– 𝐴) ∩ (V βˆ– 𝐢))))
2220, 21eqtr4i 2761 . . . 4 ((𝐴 βˆͺ 𝐡) ∩ (𝐴 βˆͺ (V βˆ– 𝐢))) = (𝐴 βˆͺ (((𝐴 βˆ– 𝐡) ∩ 𝐢) βˆͺ ((𝐡 βˆ– 𝐴) ∩ (V βˆ– 𝐢))))
23 unass 4167 . . . . . 6 (((𝐴 ∩ 𝐢) βˆͺ 𝐡) βˆͺ 𝐡) = ((𝐴 ∩ 𝐢) βˆͺ (𝐡 βˆͺ 𝐡))
24 undi 4275 . . . . . . . . 9 (𝐡 βˆͺ (𝐴 ∩ 𝐢)) = ((𝐡 βˆͺ 𝐴) ∩ (𝐡 βˆͺ 𝐢))
25 uncom 4154 . . . . . . . . 9 ((𝐴 ∩ 𝐢) βˆͺ 𝐡) = (𝐡 βˆͺ (𝐴 ∩ 𝐢))
26 undif2 4477 . . . . . . . . . 10 (𝐡 βˆͺ (𝐴 βˆ– 𝐡)) = (𝐡 βˆͺ 𝐴)
2726ineq1i 4209 . . . . . . . . 9 ((𝐡 βˆͺ (𝐴 βˆ– 𝐡)) ∩ (𝐡 βˆͺ 𝐢)) = ((𝐡 βˆͺ 𝐴) ∩ (𝐡 βˆͺ 𝐢))
2824, 25, 273eqtr4i 2768 . . . . . . . 8 ((𝐴 ∩ 𝐢) βˆͺ 𝐡) = ((𝐡 βˆͺ (𝐴 βˆ– 𝐡)) ∩ (𝐡 βˆͺ 𝐢))
29 undi 4275 . . . . . . . 8 (𝐡 βˆͺ ((𝐴 βˆ– 𝐡) ∩ 𝐢)) = ((𝐡 βˆͺ (𝐴 βˆ– 𝐡)) ∩ (𝐡 βˆͺ 𝐢))
3028, 29eqtr4i 2761 . . . . . . 7 ((𝐴 ∩ 𝐢) βˆͺ 𝐡) = (𝐡 βˆͺ ((𝐴 βˆ– 𝐡) ∩ 𝐢))
31 undi 4275 . . . . . . . 8 (𝐡 βˆͺ ((𝐡 βˆ– 𝐴) ∩ (V βˆ– 𝐢))) = ((𝐡 βˆͺ (𝐡 βˆ– 𝐴)) ∩ (𝐡 βˆͺ (V βˆ– 𝐢)))
32 undifabs 4478 . . . . . . . . 9 (𝐡 βˆͺ (𝐡 βˆ– 𝐴)) = 𝐡
3332ineq1i 4209 . . . . . . . 8 ((𝐡 βˆͺ (𝐡 βˆ– 𝐴)) ∩ (𝐡 βˆͺ (V βˆ– 𝐢))) = (𝐡 ∩ (𝐡 βˆͺ (V βˆ– 𝐢)))
34 inabs 4256 . . . . . . . 8 (𝐡 ∩ (𝐡 βˆͺ (V βˆ– 𝐢))) = 𝐡
3531, 33, 343eqtrri 2763 . . . . . . 7 𝐡 = (𝐡 βˆͺ ((𝐡 βˆ– 𝐴) ∩ (V βˆ– 𝐢)))
3630, 35uneq12i 4162 . . . . . 6 (((𝐴 ∩ 𝐢) βˆͺ 𝐡) βˆͺ 𝐡) = ((𝐡 βˆͺ ((𝐴 βˆ– 𝐡) ∩ 𝐢)) βˆͺ (𝐡 βˆͺ ((𝐡 βˆ– 𝐴) ∩ (V βˆ– 𝐢))))
37 unidm 4153 . . . . . . 7 (𝐡 βˆͺ 𝐡) = 𝐡
3837uneq2i 4161 . . . . . 6 ((𝐴 ∩ 𝐢) βˆͺ (𝐡 βˆͺ 𝐡)) = ((𝐴 ∩ 𝐢) βˆͺ 𝐡)
3923, 36, 383eqtr3ri 2767 . . . . 5 ((𝐴 ∩ 𝐢) βˆͺ 𝐡) = ((𝐡 βˆͺ ((𝐴 βˆ– 𝐡) ∩ 𝐢)) βˆͺ (𝐡 βˆͺ ((𝐡 βˆ– 𝐴) ∩ (V βˆ– 𝐢))))
40 uncom 4154 . . . . . . 7 (𝐡 βˆͺ 𝐢) = (𝐢 βˆͺ 𝐡)
4140ineq2i 4210 . . . . . 6 ((𝐴 βˆͺ 𝐡) ∩ (𝐡 βˆͺ 𝐢)) = ((𝐴 βˆͺ 𝐡) ∩ (𝐢 βˆͺ 𝐡))
42 undir 4277 . . . . . 6 ((𝐴 ∩ 𝐢) βˆͺ 𝐡) = ((𝐴 βˆͺ 𝐡) ∩ (𝐢 βˆͺ 𝐡))
4341, 42eqtr4i 2761 . . . . 5 ((𝐴 βˆͺ 𝐡) ∩ (𝐡 βˆͺ 𝐢)) = ((𝐴 ∩ 𝐢) βˆͺ 𝐡)
44 unundi 4171 . . . . 5 (𝐡 βˆͺ (((𝐴 βˆ– 𝐡) ∩ 𝐢) βˆͺ ((𝐡 βˆ– 𝐴) ∩ (V βˆ– 𝐢)))) = ((𝐡 βˆͺ ((𝐴 βˆ– 𝐡) ∩ 𝐢)) βˆͺ (𝐡 βˆͺ ((𝐡 βˆ– 𝐴) ∩ (V βˆ– 𝐢))))
4539, 43, 443eqtr4i 2768 . . . 4 ((𝐴 βˆͺ 𝐡) ∩ (𝐡 βˆͺ 𝐢)) = (𝐡 βˆͺ (((𝐴 βˆ– 𝐡) ∩ 𝐢) βˆͺ ((𝐡 βˆ– 𝐴) ∩ (V βˆ– 𝐢))))
4622, 45ineq12i 4211 . . 3 (((𝐴 βˆͺ 𝐡) ∩ (𝐴 βˆͺ (V βˆ– 𝐢))) ∩ ((𝐴 βˆͺ 𝐡) ∩ (𝐡 βˆͺ 𝐢))) = ((𝐴 βˆͺ (((𝐴 βˆ– 𝐡) ∩ 𝐢) βˆͺ ((𝐡 βˆ– 𝐴) ∩ (V βˆ– 𝐢)))) ∩ (𝐡 βˆͺ (((𝐴 βˆ– 𝐡) ∩ 𝐢) βˆͺ ((𝐡 βˆ– 𝐴) ∩ (V βˆ– 𝐢)))))
474, 46eqtr4i 2761 . 2 ((𝐴 ∩ 𝐡) βˆͺ (((𝐴 βˆ– 𝐡) ∩ 𝐢) βˆͺ ((𝐡 βˆ– 𝐴) ∩ (V βˆ– 𝐢)))) = (((𝐴 βˆͺ 𝐡) ∩ (𝐴 βˆͺ (V βˆ– 𝐢))) ∩ ((𝐴 βˆͺ 𝐡) ∩ (𝐡 βˆͺ 𝐢)))
481, 3, 473eqtr4i 2768 1 if(πœ‘, 𝐴, 𝐡) = ((𝐴 ∩ 𝐡) βˆͺ (((𝐴 βˆ– 𝐡) ∩ 𝐢) βˆͺ ((𝐡 βˆ– 𝐴) ∩ (V βˆ– 𝐢))))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1539  {cab 2707  Vcvv 3472   βˆ– cdif 3946   βˆͺ cun 3947   ∩ cin 3948  ifcif 4529
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator