ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  uniuni GIF version

Theorem uniuni 4448
Description: Expression for double union that moves union into a class builder. (Contributed by FL, 28-May-2007.)
Assertion
Ref Expression
uniuni 𝐴 = {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)}
Distinct variable group:   𝑥,𝐴,𝑦

Proof of Theorem uniuni
Dummy variables 𝑣 𝑧 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eluni 3810 . . . . . 6 (𝑢 𝐴 ↔ ∃𝑦(𝑢𝑦𝑦𝐴))
21anbi2i 457 . . . . 5 ((𝑧𝑢𝑢 𝐴) ↔ (𝑧𝑢 ∧ ∃𝑦(𝑢𝑦𝑦𝐴)))
32exbii 1605 . . . 4 (∃𝑢(𝑧𝑢𝑢 𝐴) ↔ ∃𝑢(𝑧𝑢 ∧ ∃𝑦(𝑢𝑦𝑦𝐴)))
4 19.42v 1906 . . . . . . 7 (∃𝑦(𝑧𝑢 ∧ (𝑢𝑦𝑦𝐴)) ↔ (𝑧𝑢 ∧ ∃𝑦(𝑢𝑦𝑦𝐴)))
54bicomi 132 . . . . . 6 ((𝑧𝑢 ∧ ∃𝑦(𝑢𝑦𝑦𝐴)) ↔ ∃𝑦(𝑧𝑢 ∧ (𝑢𝑦𝑦𝐴)))
65exbii 1605 . . . . 5 (∃𝑢(𝑧𝑢 ∧ ∃𝑦(𝑢𝑦𝑦𝐴)) ↔ ∃𝑢𝑦(𝑧𝑢 ∧ (𝑢𝑦𝑦𝐴)))
7 excom 1664 . . . . . 6 (∃𝑢𝑦(𝑧𝑢 ∧ (𝑢𝑦𝑦𝐴)) ↔ ∃𝑦𝑢(𝑧𝑢 ∧ (𝑢𝑦𝑦𝐴)))
8 anass 401 . . . . . . . 8 (((𝑧𝑢𝑢𝑦) ∧ 𝑦𝐴) ↔ (𝑧𝑢 ∧ (𝑢𝑦𝑦𝐴)))
9 ancom 266 . . . . . . . 8 (((𝑧𝑢𝑢𝑦) ∧ 𝑦𝐴) ↔ (𝑦𝐴 ∧ (𝑧𝑢𝑢𝑦)))
108, 9bitr3i 186 . . . . . . 7 ((𝑧𝑢 ∧ (𝑢𝑦𝑦𝐴)) ↔ (𝑦𝐴 ∧ (𝑧𝑢𝑢𝑦)))
11102exbii 1606 . . . . . 6 (∃𝑦𝑢(𝑧𝑢 ∧ (𝑢𝑦𝑦𝐴)) ↔ ∃𝑦𝑢(𝑦𝐴 ∧ (𝑧𝑢𝑢𝑦)))
12 exdistr 1909 . . . . . 6 (∃𝑦𝑢(𝑦𝐴 ∧ (𝑧𝑢𝑢𝑦)) ↔ ∃𝑦(𝑦𝐴 ∧ ∃𝑢(𝑧𝑢𝑢𝑦)))
137, 11, 123bitri 206 . . . . 5 (∃𝑢𝑦(𝑧𝑢 ∧ (𝑢𝑦𝑦𝐴)) ↔ ∃𝑦(𝑦𝐴 ∧ ∃𝑢(𝑧𝑢𝑢𝑦)))
14 eluni 3810 . . . . . . . 8 (𝑧 𝑦 ↔ ∃𝑢(𝑧𝑢𝑢𝑦))
1514bicomi 132 . . . . . . 7 (∃𝑢(𝑧𝑢𝑢𝑦) ↔ 𝑧 𝑦)
1615anbi2i 457 . . . . . 6 ((𝑦𝐴 ∧ ∃𝑢(𝑧𝑢𝑢𝑦)) ↔ (𝑦𝐴𝑧 𝑦))
1716exbii 1605 . . . . 5 (∃𝑦(𝑦𝐴 ∧ ∃𝑢(𝑧𝑢𝑢𝑦)) ↔ ∃𝑦(𝑦𝐴𝑧 𝑦))
186, 13, 173bitri 206 . . . 4 (∃𝑢(𝑧𝑢 ∧ ∃𝑦(𝑢𝑦𝑦𝐴)) ↔ ∃𝑦(𝑦𝐴𝑧 𝑦))
19 vex 2740 . . . . . . . . . . 11 𝑦 ∈ V
2019uniex 4434 . . . . . . . . . 10 𝑦 ∈ V
21 eleq2 2241 . . . . . . . . . 10 (𝑣 = 𝑦 → (𝑧𝑣𝑧 𝑦))
2220, 21ceqsexv 2776 . . . . . . . . 9 (∃𝑣(𝑣 = 𝑦𝑧𝑣) ↔ 𝑧 𝑦)
23 exancom 1608 . . . . . . . . 9 (∃𝑣(𝑣 = 𝑦𝑧𝑣) ↔ ∃𝑣(𝑧𝑣𝑣 = 𝑦))
2422, 23bitr3i 186 . . . . . . . 8 (𝑧 𝑦 ↔ ∃𝑣(𝑧𝑣𝑣 = 𝑦))
2524anbi2i 457 . . . . . . 7 ((𝑦𝐴𝑧 𝑦) ↔ (𝑦𝐴 ∧ ∃𝑣(𝑧𝑣𝑣 = 𝑦)))
26 19.42v 1906 . . . . . . 7 (∃𝑣(𝑦𝐴 ∧ (𝑧𝑣𝑣 = 𝑦)) ↔ (𝑦𝐴 ∧ ∃𝑣(𝑧𝑣𝑣 = 𝑦)))
27 ancom 266 . . . . . . . . 9 ((𝑦𝐴 ∧ (𝑧𝑣𝑣 = 𝑦)) ↔ ((𝑧𝑣𝑣 = 𝑦) ∧ 𝑦𝐴))
28 anass 401 . . . . . . . . 9 (((𝑧𝑣𝑣 = 𝑦) ∧ 𝑦𝐴) ↔ (𝑧𝑣 ∧ (𝑣 = 𝑦𝑦𝐴)))
2927, 28bitri 184 . . . . . . . 8 ((𝑦𝐴 ∧ (𝑧𝑣𝑣 = 𝑦)) ↔ (𝑧𝑣 ∧ (𝑣 = 𝑦𝑦𝐴)))
3029exbii 1605 . . . . . . 7 (∃𝑣(𝑦𝐴 ∧ (𝑧𝑣𝑣 = 𝑦)) ↔ ∃𝑣(𝑧𝑣 ∧ (𝑣 = 𝑦𝑦𝐴)))
3125, 26, 303bitr2i 208 . . . . . 6 ((𝑦𝐴𝑧 𝑦) ↔ ∃𝑣(𝑧𝑣 ∧ (𝑣 = 𝑦𝑦𝐴)))
3231exbii 1605 . . . . 5 (∃𝑦(𝑦𝐴𝑧 𝑦) ↔ ∃𝑦𝑣(𝑧𝑣 ∧ (𝑣 = 𝑦𝑦𝐴)))
33 excom 1664 . . . . 5 (∃𝑦𝑣(𝑧𝑣 ∧ (𝑣 = 𝑦𝑦𝐴)) ↔ ∃𝑣𝑦(𝑧𝑣 ∧ (𝑣 = 𝑦𝑦𝐴)))
34 exdistr 1909 . . . . . 6 (∃𝑣𝑦(𝑧𝑣 ∧ (𝑣 = 𝑦𝑦𝐴)) ↔ ∃𝑣(𝑧𝑣 ∧ ∃𝑦(𝑣 = 𝑦𝑦𝐴)))
35 vex 2740 . . . . . . . . . 10 𝑣 ∈ V
36 eqeq1 2184 . . . . . . . . . . . 12 (𝑥 = 𝑣 → (𝑥 = 𝑦𝑣 = 𝑦))
3736anbi1d 465 . . . . . . . . . . 11 (𝑥 = 𝑣 → ((𝑥 = 𝑦𝑦𝐴) ↔ (𝑣 = 𝑦𝑦𝐴)))
3837exbidv 1825 . . . . . . . . . 10 (𝑥 = 𝑣 → (∃𝑦(𝑥 = 𝑦𝑦𝐴) ↔ ∃𝑦(𝑣 = 𝑦𝑦𝐴)))
3935, 38elab 2881 . . . . . . . . 9 (𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)} ↔ ∃𝑦(𝑣 = 𝑦𝑦𝐴))
4039bicomi 132 . . . . . . . 8 (∃𝑦(𝑣 = 𝑦𝑦𝐴) ↔ 𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)})
4140anbi2i 457 . . . . . . 7 ((𝑧𝑣 ∧ ∃𝑦(𝑣 = 𝑦𝑦𝐴)) ↔ (𝑧𝑣𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)}))
4241exbii 1605 . . . . . 6 (∃𝑣(𝑧𝑣 ∧ ∃𝑦(𝑣 = 𝑦𝑦𝐴)) ↔ ∃𝑣(𝑧𝑣𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)}))
4334, 42bitri 184 . . . . 5 (∃𝑣𝑦(𝑧𝑣 ∧ (𝑣 = 𝑦𝑦𝐴)) ↔ ∃𝑣(𝑧𝑣𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)}))
4432, 33, 433bitri 206 . . . 4 (∃𝑦(𝑦𝐴𝑧 𝑦) ↔ ∃𝑣(𝑧𝑣𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)}))
453, 18, 443bitri 206 . . 3 (∃𝑢(𝑧𝑢𝑢 𝐴) ↔ ∃𝑣(𝑧𝑣𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)}))
4645abbii 2293 . 2 {𝑧 ∣ ∃𝑢(𝑧𝑢𝑢 𝐴)} = {𝑧 ∣ ∃𝑣(𝑧𝑣𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)})}
47 df-uni 3808 . 2 𝐴 = {𝑧 ∣ ∃𝑢(𝑧𝑢𝑢 𝐴)}
48 df-uni 3808 . 2 {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)} = {𝑧 ∣ ∃𝑣(𝑧𝑣𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)})}
4946, 47, 483eqtr4i 2208 1 𝐴 = {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)}
Colors of variables: wff set class
Syntax hints:  wa 104   = wceq 1353  wex 1492  wcel 2148  {cab 2163   cuni 3807
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4118  ax-un 4430
This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-v 2739  df-uni 3808
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator