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

Theorem uniuni 4463
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 3824 . . . . . 6 (𝑢 𝐴 ↔ ∃𝑦(𝑢𝑦𝑦𝐴))
21anbi2i 457 . . . . 5 ((𝑧𝑢𝑢 𝐴) ↔ (𝑧𝑢 ∧ ∃𝑦(𝑢𝑦𝑦𝐴)))
32exbii 1615 . . . 4 (∃𝑢(𝑧𝑢𝑢 𝐴) ↔ ∃𝑢(𝑧𝑢 ∧ ∃𝑦(𝑢𝑦𝑦𝐴)))
4 19.42v 1916 . . . . . . 7 (∃𝑦(𝑧𝑢 ∧ (𝑢𝑦𝑦𝐴)) ↔ (𝑧𝑢 ∧ ∃𝑦(𝑢𝑦𝑦𝐴)))
54bicomi 132 . . . . . 6 ((𝑧𝑢 ∧ ∃𝑦(𝑢𝑦𝑦𝐴)) ↔ ∃𝑦(𝑧𝑢 ∧ (𝑢𝑦𝑦𝐴)))
65exbii 1615 . . . . 5 (∃𝑢(𝑧𝑢 ∧ ∃𝑦(𝑢𝑦𝑦𝐴)) ↔ ∃𝑢𝑦(𝑧𝑢 ∧ (𝑢𝑦𝑦𝐴)))
7 excom 1674 . . . . . 6 (∃𝑢𝑦(𝑧𝑢 ∧ (𝑢𝑦𝑦𝐴)) ↔ ∃𝑦𝑢(𝑧𝑢 ∧ (𝑢𝑦𝑦𝐴)))
8 anass 401 . . . . . . . 8 (((𝑧𝑢𝑢𝑦) ∧ 𝑦𝐴) ↔ (𝑧𝑢 ∧ (𝑢𝑦𝑦𝐴)))
9 ancom 266 . . . . . . . 8 (((𝑧𝑢𝑢𝑦) ∧ 𝑦𝐴) ↔ (𝑦𝐴 ∧ (𝑧𝑢𝑢𝑦)))
108, 9bitr3i 186 . . . . . . 7 ((𝑧𝑢 ∧ (𝑢𝑦𝑦𝐴)) ↔ (𝑦𝐴 ∧ (𝑧𝑢𝑢𝑦)))
11102exbii 1616 . . . . . 6 (∃𝑦𝑢(𝑧𝑢 ∧ (𝑢𝑦𝑦𝐴)) ↔ ∃𝑦𝑢(𝑦𝐴 ∧ (𝑧𝑢𝑢𝑦)))
12 exdistr 1919 . . . . . 6 (∃𝑦𝑢(𝑦𝐴 ∧ (𝑧𝑢𝑢𝑦)) ↔ ∃𝑦(𝑦𝐴 ∧ ∃𝑢(𝑧𝑢𝑢𝑦)))
137, 11, 123bitri 206 . . . . 5 (∃𝑢𝑦(𝑧𝑢 ∧ (𝑢𝑦𝑦𝐴)) ↔ ∃𝑦(𝑦𝐴 ∧ ∃𝑢(𝑧𝑢𝑢𝑦)))
14 eluni 3824 . . . . . . . 8 (𝑧 𝑦 ↔ ∃𝑢(𝑧𝑢𝑢𝑦))
1514bicomi 132 . . . . . . 7 (∃𝑢(𝑧𝑢𝑢𝑦) ↔ 𝑧 𝑦)
1615anbi2i 457 . . . . . 6 ((𝑦𝐴 ∧ ∃𝑢(𝑧𝑢𝑢𝑦)) ↔ (𝑦𝐴𝑧 𝑦))
1716exbii 1615 . . . . 5 (∃𝑦(𝑦𝐴 ∧ ∃𝑢(𝑧𝑢𝑢𝑦)) ↔ ∃𝑦(𝑦𝐴𝑧 𝑦))
186, 13, 173bitri 206 . . . 4 (∃𝑢(𝑧𝑢 ∧ ∃𝑦(𝑢𝑦𝑦𝐴)) ↔ ∃𝑦(𝑦𝐴𝑧 𝑦))
19 vex 2752 . . . . . . . . . . 11 𝑦 ∈ V
2019uniex 4449 . . . . . . . . . 10 𝑦 ∈ V
21 eleq2 2251 . . . . . . . . . 10 (𝑣 = 𝑦 → (𝑧𝑣𝑧 𝑦))
2220, 21ceqsexv 2788 . . . . . . . . 9 (∃𝑣(𝑣 = 𝑦𝑧𝑣) ↔ 𝑧 𝑦)
23 exancom 1618 . . . . . . . . 9 (∃𝑣(𝑣 = 𝑦𝑧𝑣) ↔ ∃𝑣(𝑧𝑣𝑣 = 𝑦))
2422, 23bitr3i 186 . . . . . . . 8 (𝑧 𝑦 ↔ ∃𝑣(𝑧𝑣𝑣 = 𝑦))
2524anbi2i 457 . . . . . . 7 ((𝑦𝐴𝑧 𝑦) ↔ (𝑦𝐴 ∧ ∃𝑣(𝑧𝑣𝑣 = 𝑦)))
26 19.42v 1916 . . . . . . 7 (∃𝑣(𝑦𝐴 ∧ (𝑧𝑣𝑣 = 𝑦)) ↔ (𝑦𝐴 ∧ ∃𝑣(𝑧𝑣𝑣 = 𝑦)))
27 ancom 266 . . . . . . . . 9 ((𝑦𝐴 ∧ (𝑧𝑣𝑣 = 𝑦)) ↔ ((𝑧𝑣𝑣 = 𝑦) ∧ 𝑦𝐴))
28 anass 401 . . . . . . . . 9 (((𝑧𝑣𝑣 = 𝑦) ∧ 𝑦𝐴) ↔ (𝑧𝑣 ∧ (𝑣 = 𝑦𝑦𝐴)))
2927, 28bitri 184 . . . . . . . 8 ((𝑦𝐴 ∧ (𝑧𝑣𝑣 = 𝑦)) ↔ (𝑧𝑣 ∧ (𝑣 = 𝑦𝑦𝐴)))
3029exbii 1615 . . . . . . 7 (∃𝑣(𝑦𝐴 ∧ (𝑧𝑣𝑣 = 𝑦)) ↔ ∃𝑣(𝑧𝑣 ∧ (𝑣 = 𝑦𝑦𝐴)))
3125, 26, 303bitr2i 208 . . . . . 6 ((𝑦𝐴𝑧 𝑦) ↔ ∃𝑣(𝑧𝑣 ∧ (𝑣 = 𝑦𝑦𝐴)))
3231exbii 1615 . . . . 5 (∃𝑦(𝑦𝐴𝑧 𝑦) ↔ ∃𝑦𝑣(𝑧𝑣 ∧ (𝑣 = 𝑦𝑦𝐴)))
33 excom 1674 . . . . 5 (∃𝑦𝑣(𝑧𝑣 ∧ (𝑣 = 𝑦𝑦𝐴)) ↔ ∃𝑣𝑦(𝑧𝑣 ∧ (𝑣 = 𝑦𝑦𝐴)))
34 exdistr 1919 . . . . . 6 (∃𝑣𝑦(𝑧𝑣 ∧ (𝑣 = 𝑦𝑦𝐴)) ↔ ∃𝑣(𝑧𝑣 ∧ ∃𝑦(𝑣 = 𝑦𝑦𝐴)))
35 vex 2752 . . . . . . . . . 10 𝑣 ∈ V
36 eqeq1 2194 . . . . . . . . . . . 12 (𝑥 = 𝑣 → (𝑥 = 𝑦𝑣 = 𝑦))
3736anbi1d 465 . . . . . . . . . . 11 (𝑥 = 𝑣 → ((𝑥 = 𝑦𝑦𝐴) ↔ (𝑣 = 𝑦𝑦𝐴)))
3837exbidv 1835 . . . . . . . . . 10 (𝑥 = 𝑣 → (∃𝑦(𝑥 = 𝑦𝑦𝐴) ↔ ∃𝑦(𝑣 = 𝑦𝑦𝐴)))
3935, 38elab 2893 . . . . . . . . 9 (𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)} ↔ ∃𝑦(𝑣 = 𝑦𝑦𝐴))
4039bicomi 132 . . . . . . . 8 (∃𝑦(𝑣 = 𝑦𝑦𝐴) ↔ 𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)})
4140anbi2i 457 . . . . . . 7 ((𝑧𝑣 ∧ ∃𝑦(𝑣 = 𝑦𝑦𝐴)) ↔ (𝑧𝑣𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)}))
4241exbii 1615 . . . . . 6 (∃𝑣(𝑧𝑣 ∧ ∃𝑦(𝑣 = 𝑦𝑦𝐴)) ↔ ∃𝑣(𝑧𝑣𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)}))
4334, 42bitri 184 . . . . 5 (∃𝑣𝑦(𝑧𝑣 ∧ (𝑣 = 𝑦𝑦𝐴)) ↔ ∃𝑣(𝑧𝑣𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)}))
4432, 33, 433bitri 206 . . . 4 (∃𝑦(𝑦𝐴𝑧 𝑦) ↔ ∃𝑣(𝑧𝑣𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)}))
453, 18, 443bitri 206 . . 3 (∃𝑢(𝑧𝑢𝑢 𝐴) ↔ ∃𝑣(𝑧𝑣𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)}))
4645abbii 2303 . 2 {𝑧 ∣ ∃𝑢(𝑧𝑢𝑢 𝐴)} = {𝑧 ∣ ∃𝑣(𝑧𝑣𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)})}
47 df-uni 3822 . 2 𝐴 = {𝑧 ∣ ∃𝑢(𝑧𝑢𝑢 𝐴)}
48 df-uni 3822 . 2 {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)} = {𝑧 ∣ ∃𝑣(𝑧𝑣𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)})}
4946, 47, 483eqtr4i 2218 1 𝐴 = {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)}
Colors of variables: wff set class
Syntax hints:  wa 104   = wceq 1363  wex 1502  wcel 2158  {cab 2173   cuni 3821
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 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-13 2160  ax-14 2161  ax-ext 2169  ax-sep 4133  ax-un 4445
This theorem depends on definitions:  df-bi 117  df-tru 1366  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-rex 2471  df-v 2751  df-uni 3822
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator