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

Theorem uniuni 4379
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 3746 . . . . . 6 (𝑢 𝐴 ↔ ∃𝑦(𝑢𝑦𝑦𝐴))
21anbi2i 453 . . . . 5 ((𝑧𝑢𝑢 𝐴) ↔ (𝑧𝑢 ∧ ∃𝑦(𝑢𝑦𝑦𝐴)))
32exbii 1585 . . . 4 (∃𝑢(𝑧𝑢𝑢 𝐴) ↔ ∃𝑢(𝑧𝑢 ∧ ∃𝑦(𝑢𝑦𝑦𝐴)))
4 19.42v 1879 . . . . . . 7 (∃𝑦(𝑧𝑢 ∧ (𝑢𝑦𝑦𝐴)) ↔ (𝑧𝑢 ∧ ∃𝑦(𝑢𝑦𝑦𝐴)))
54bicomi 131 . . . . . 6 ((𝑧𝑢 ∧ ∃𝑦(𝑢𝑦𝑦𝐴)) ↔ ∃𝑦(𝑧𝑢 ∧ (𝑢𝑦𝑦𝐴)))
65exbii 1585 . . . . 5 (∃𝑢(𝑧𝑢 ∧ ∃𝑦(𝑢𝑦𝑦𝐴)) ↔ ∃𝑢𝑦(𝑧𝑢 ∧ (𝑢𝑦𝑦𝐴)))
7 excom 1643 . . . . . 6 (∃𝑢𝑦(𝑧𝑢 ∧ (𝑢𝑦𝑦𝐴)) ↔ ∃𝑦𝑢(𝑧𝑢 ∧ (𝑢𝑦𝑦𝐴)))
8 anass 399 . . . . . . . 8 (((𝑧𝑢𝑢𝑦) ∧ 𝑦𝐴) ↔ (𝑧𝑢 ∧ (𝑢𝑦𝑦𝐴)))
9 ancom 264 . . . . . . . 8 (((𝑧𝑢𝑢𝑦) ∧ 𝑦𝐴) ↔ (𝑦𝐴 ∧ (𝑧𝑢𝑢𝑦)))
108, 9bitr3i 185 . . . . . . 7 ((𝑧𝑢 ∧ (𝑢𝑦𝑦𝐴)) ↔ (𝑦𝐴 ∧ (𝑧𝑢𝑢𝑦)))
11102exbii 1586 . . . . . 6 (∃𝑦𝑢(𝑧𝑢 ∧ (𝑢𝑦𝑦𝐴)) ↔ ∃𝑦𝑢(𝑦𝐴 ∧ (𝑧𝑢𝑢𝑦)))
12 exdistr 1882 . . . . . 6 (∃𝑦𝑢(𝑦𝐴 ∧ (𝑧𝑢𝑢𝑦)) ↔ ∃𝑦(𝑦𝐴 ∧ ∃𝑢(𝑧𝑢𝑢𝑦)))
137, 11, 123bitri 205 . . . . 5 (∃𝑢𝑦(𝑧𝑢 ∧ (𝑢𝑦𝑦𝐴)) ↔ ∃𝑦(𝑦𝐴 ∧ ∃𝑢(𝑧𝑢𝑢𝑦)))
14 eluni 3746 . . . . . . . 8 (𝑧 𝑦 ↔ ∃𝑢(𝑧𝑢𝑢𝑦))
1514bicomi 131 . . . . . . 7 (∃𝑢(𝑧𝑢𝑢𝑦) ↔ 𝑧 𝑦)
1615anbi2i 453 . . . . . 6 ((𝑦𝐴 ∧ ∃𝑢(𝑧𝑢𝑢𝑦)) ↔ (𝑦𝐴𝑧 𝑦))
1716exbii 1585 . . . . 5 (∃𝑦(𝑦𝐴 ∧ ∃𝑢(𝑧𝑢𝑢𝑦)) ↔ ∃𝑦(𝑦𝐴𝑧 𝑦))
186, 13, 173bitri 205 . . . 4 (∃𝑢(𝑧𝑢 ∧ ∃𝑦(𝑢𝑦𝑦𝐴)) ↔ ∃𝑦(𝑦𝐴𝑧 𝑦))
19 vex 2692 . . . . . . . . . . 11 𝑦 ∈ V
2019uniex 4366 . . . . . . . . . 10 𝑦 ∈ V
21 eleq2 2204 . . . . . . . . . 10 (𝑣 = 𝑦 → (𝑧𝑣𝑧 𝑦))
2220, 21ceqsexv 2728 . . . . . . . . 9 (∃𝑣(𝑣 = 𝑦𝑧𝑣) ↔ 𝑧 𝑦)
23 exancom 1588 . . . . . . . . 9 (∃𝑣(𝑣 = 𝑦𝑧𝑣) ↔ ∃𝑣(𝑧𝑣𝑣 = 𝑦))
2422, 23bitr3i 185 . . . . . . . 8 (𝑧 𝑦 ↔ ∃𝑣(𝑧𝑣𝑣 = 𝑦))
2524anbi2i 453 . . . . . . 7 ((𝑦𝐴𝑧 𝑦) ↔ (𝑦𝐴 ∧ ∃𝑣(𝑧𝑣𝑣 = 𝑦)))
26 19.42v 1879 . . . . . . 7 (∃𝑣(𝑦𝐴 ∧ (𝑧𝑣𝑣 = 𝑦)) ↔ (𝑦𝐴 ∧ ∃𝑣(𝑧𝑣𝑣 = 𝑦)))
27 ancom 264 . . . . . . . . 9 ((𝑦𝐴 ∧ (𝑧𝑣𝑣 = 𝑦)) ↔ ((𝑧𝑣𝑣 = 𝑦) ∧ 𝑦𝐴))
28 anass 399 . . . . . . . . 9 (((𝑧𝑣𝑣 = 𝑦) ∧ 𝑦𝐴) ↔ (𝑧𝑣 ∧ (𝑣 = 𝑦𝑦𝐴)))
2927, 28bitri 183 . . . . . . . 8 ((𝑦𝐴 ∧ (𝑧𝑣𝑣 = 𝑦)) ↔ (𝑧𝑣 ∧ (𝑣 = 𝑦𝑦𝐴)))
3029exbii 1585 . . . . . . 7 (∃𝑣(𝑦𝐴 ∧ (𝑧𝑣𝑣 = 𝑦)) ↔ ∃𝑣(𝑧𝑣 ∧ (𝑣 = 𝑦𝑦𝐴)))
3125, 26, 303bitr2i 207 . . . . . 6 ((𝑦𝐴𝑧 𝑦) ↔ ∃𝑣(𝑧𝑣 ∧ (𝑣 = 𝑦𝑦𝐴)))
3231exbii 1585 . . . . 5 (∃𝑦(𝑦𝐴𝑧 𝑦) ↔ ∃𝑦𝑣(𝑧𝑣 ∧ (𝑣 = 𝑦𝑦𝐴)))
33 excom 1643 . . . . 5 (∃𝑦𝑣(𝑧𝑣 ∧ (𝑣 = 𝑦𝑦𝐴)) ↔ ∃𝑣𝑦(𝑧𝑣 ∧ (𝑣 = 𝑦𝑦𝐴)))
34 exdistr 1882 . . . . . 6 (∃𝑣𝑦(𝑧𝑣 ∧ (𝑣 = 𝑦𝑦𝐴)) ↔ ∃𝑣(𝑧𝑣 ∧ ∃𝑦(𝑣 = 𝑦𝑦𝐴)))
35 vex 2692 . . . . . . . . . 10 𝑣 ∈ V
36 eqeq1 2147 . . . . . . . . . . . 12 (𝑥 = 𝑣 → (𝑥 = 𝑦𝑣 = 𝑦))
3736anbi1d 461 . . . . . . . . . . 11 (𝑥 = 𝑣 → ((𝑥 = 𝑦𝑦𝐴) ↔ (𝑣 = 𝑦𝑦𝐴)))
3837exbidv 1798 . . . . . . . . . 10 (𝑥 = 𝑣 → (∃𝑦(𝑥 = 𝑦𝑦𝐴) ↔ ∃𝑦(𝑣 = 𝑦𝑦𝐴)))
3935, 38elab 2831 . . . . . . . . 9 (𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)} ↔ ∃𝑦(𝑣 = 𝑦𝑦𝐴))
4039bicomi 131 . . . . . . . 8 (∃𝑦(𝑣 = 𝑦𝑦𝐴) ↔ 𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)})
4140anbi2i 453 . . . . . . 7 ((𝑧𝑣 ∧ ∃𝑦(𝑣 = 𝑦𝑦𝐴)) ↔ (𝑧𝑣𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)}))
4241exbii 1585 . . . . . 6 (∃𝑣(𝑧𝑣 ∧ ∃𝑦(𝑣 = 𝑦𝑦𝐴)) ↔ ∃𝑣(𝑧𝑣𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)}))
4334, 42bitri 183 . . . . 5 (∃𝑣𝑦(𝑧𝑣 ∧ (𝑣 = 𝑦𝑦𝐴)) ↔ ∃𝑣(𝑧𝑣𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)}))
4432, 33, 433bitri 205 . . . 4 (∃𝑦(𝑦𝐴𝑧 𝑦) ↔ ∃𝑣(𝑧𝑣𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)}))
453, 18, 443bitri 205 . . 3 (∃𝑢(𝑧𝑢𝑢 𝐴) ↔ ∃𝑣(𝑧𝑣𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)}))
4645abbii 2256 . 2 {𝑧 ∣ ∃𝑢(𝑧𝑢𝑢 𝐴)} = {𝑧 ∣ ∃𝑣(𝑧𝑣𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)})}
47 df-uni 3744 . 2 𝐴 = {𝑧 ∣ ∃𝑢(𝑧𝑢𝑢 𝐴)}
48 df-uni 3744 . 2 {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)} = {𝑧 ∣ ∃𝑣(𝑧𝑣𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)})}
4946, 47, 483eqtr4i 2171 1 𝐴 = {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)}
Colors of variables: wff set class
Syntax hints:  wa 103   = wceq 1332  wex 1469  wcel 1481  {cab 2126   cuni 3743
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4053  ax-un 4362
This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-rex 2423  df-v 2691  df-uni 3744
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator