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

Theorem uniuni 6865
 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 4375 . . . . . 6 (𝑢 𝐴 ↔ ∃𝑦(𝑢𝑦𝑦𝐴))
21anbi2i 726 . . . . 5 ((𝑧𝑢𝑢 𝐴) ↔ (𝑧𝑢 ∧ ∃𝑦(𝑢𝑦𝑦𝐴)))
32exbii 1764 . . . 4 (∃𝑢(𝑧𝑢𝑢 𝐴) ↔ ∃𝑢(𝑧𝑢 ∧ ∃𝑦(𝑢𝑦𝑦𝐴)))
4 19.42v 1905 . . . . . . 7 (∃𝑦(𝑧𝑢 ∧ (𝑢𝑦𝑦𝐴)) ↔ (𝑧𝑢 ∧ ∃𝑦(𝑢𝑦𝑦𝐴)))
54bicomi 213 . . . . . 6 ((𝑧𝑢 ∧ ∃𝑦(𝑢𝑦𝑦𝐴)) ↔ ∃𝑦(𝑧𝑢 ∧ (𝑢𝑦𝑦𝐴)))
65exbii 1764 . . . . 5 (∃𝑢(𝑧𝑢 ∧ ∃𝑦(𝑢𝑦𝑦𝐴)) ↔ ∃𝑢𝑦(𝑧𝑢 ∧ (𝑢𝑦𝑦𝐴)))
7 excom 2029 . . . . . 6 (∃𝑢𝑦(𝑧𝑢 ∧ (𝑢𝑦𝑦𝐴)) ↔ ∃𝑦𝑢(𝑧𝑢 ∧ (𝑢𝑦𝑦𝐴)))
8 anass 679 . . . . . . . 8 (((𝑧𝑢𝑢𝑦) ∧ 𝑦𝐴) ↔ (𝑧𝑢 ∧ (𝑢𝑦𝑦𝐴)))
9 ancom 465 . . . . . . . 8 (((𝑧𝑢𝑢𝑦) ∧ 𝑦𝐴) ↔ (𝑦𝐴 ∧ (𝑧𝑢𝑢𝑦)))
108, 9bitr3i 265 . . . . . . 7 ((𝑧𝑢 ∧ (𝑢𝑦𝑦𝐴)) ↔ (𝑦𝐴 ∧ (𝑧𝑢𝑢𝑦)))
11102exbii 1765 . . . . . 6 (∃𝑦𝑢(𝑧𝑢 ∧ (𝑢𝑦𝑦𝐴)) ↔ ∃𝑦𝑢(𝑦𝐴 ∧ (𝑧𝑢𝑢𝑦)))
12 exdistr 1906 . . . . . 6 (∃𝑦𝑢(𝑦𝐴 ∧ (𝑧𝑢𝑢𝑦)) ↔ ∃𝑦(𝑦𝐴 ∧ ∃𝑢(𝑧𝑢𝑢𝑦)))
137, 11, 123bitri 285 . . . . 5 (∃𝑢𝑦(𝑧𝑢 ∧ (𝑢𝑦𝑦𝐴)) ↔ ∃𝑦(𝑦𝐴 ∧ ∃𝑢(𝑧𝑢𝑢𝑦)))
14 eluni 4375 . . . . . . . 8 (𝑧 𝑦 ↔ ∃𝑢(𝑧𝑢𝑢𝑦))
1514bicomi 213 . . . . . . 7 (∃𝑢(𝑧𝑢𝑢𝑦) ↔ 𝑧 𝑦)
1615anbi2i 726 . . . . . 6 ((𝑦𝐴 ∧ ∃𝑢(𝑧𝑢𝑢𝑦)) ↔ (𝑦𝐴𝑧 𝑦))
1716exbii 1764 . . . . 5 (∃𝑦(𝑦𝐴 ∧ ∃𝑢(𝑧𝑢𝑢𝑦)) ↔ ∃𝑦(𝑦𝐴𝑧 𝑦))
186, 13, 173bitri 285 . . . 4 (∃𝑢(𝑧𝑢 ∧ ∃𝑦(𝑢𝑦𝑦𝐴)) ↔ ∃𝑦(𝑦𝐴𝑧 𝑦))
19 vuniex 6852 . . . . . . . . . 10 𝑦 ∈ V
20 eleq2 2677 . . . . . . . . . 10 (𝑣 = 𝑦 → (𝑧𝑣𝑧 𝑦))
2119, 20ceqsexv 3215 . . . . . . . . 9 (∃𝑣(𝑣 = 𝑦𝑧𝑣) ↔ 𝑧 𝑦)
22 exancom 1774 . . . . . . . . 9 (∃𝑣(𝑣 = 𝑦𝑧𝑣) ↔ ∃𝑣(𝑧𝑣𝑣 = 𝑦))
2321, 22bitr3i 265 . . . . . . . 8 (𝑧 𝑦 ↔ ∃𝑣(𝑧𝑣𝑣 = 𝑦))
2423anbi2i 726 . . . . . . 7 ((𝑦𝐴𝑧 𝑦) ↔ (𝑦𝐴 ∧ ∃𝑣(𝑧𝑣𝑣 = 𝑦)))
25 19.42v 1905 . . . . . . 7 (∃𝑣(𝑦𝐴 ∧ (𝑧𝑣𝑣 = 𝑦)) ↔ (𝑦𝐴 ∧ ∃𝑣(𝑧𝑣𝑣 = 𝑦)))
26 ancom 465 . . . . . . . . 9 ((𝑦𝐴 ∧ (𝑧𝑣𝑣 = 𝑦)) ↔ ((𝑧𝑣𝑣 = 𝑦) ∧ 𝑦𝐴))
27 anass 679 . . . . . . . . 9 (((𝑧𝑣𝑣 = 𝑦) ∧ 𝑦𝐴) ↔ (𝑧𝑣 ∧ (𝑣 = 𝑦𝑦𝐴)))
2826, 27bitri 263 . . . . . . . 8 ((𝑦𝐴 ∧ (𝑧𝑣𝑣 = 𝑦)) ↔ (𝑧𝑣 ∧ (𝑣 = 𝑦𝑦𝐴)))
2928exbii 1764 . . . . . . 7 (∃𝑣(𝑦𝐴 ∧ (𝑧𝑣𝑣 = 𝑦)) ↔ ∃𝑣(𝑧𝑣 ∧ (𝑣 = 𝑦𝑦𝐴)))
3024, 25, 293bitr2i 287 . . . . . 6 ((𝑦𝐴𝑧 𝑦) ↔ ∃𝑣(𝑧𝑣 ∧ (𝑣 = 𝑦𝑦𝐴)))
3130exbii 1764 . . . . 5 (∃𝑦(𝑦𝐴𝑧 𝑦) ↔ ∃𝑦𝑣(𝑧𝑣 ∧ (𝑣 = 𝑦𝑦𝐴)))
32 excom 2029 . . . . 5 (∃𝑦𝑣(𝑧𝑣 ∧ (𝑣 = 𝑦𝑦𝐴)) ↔ ∃𝑣𝑦(𝑧𝑣 ∧ (𝑣 = 𝑦𝑦𝐴)))
33 exdistr 1906 . . . . . 6 (∃𝑣𝑦(𝑧𝑣 ∧ (𝑣 = 𝑦𝑦𝐴)) ↔ ∃𝑣(𝑧𝑣 ∧ ∃𝑦(𝑣 = 𝑦𝑦𝐴)))
34 vex 3176 . . . . . . . . . 10 𝑣 ∈ V
35 eqeq1 2614 . . . . . . . . . . . 12 (𝑥 = 𝑣 → (𝑥 = 𝑦𝑣 = 𝑦))
3635anbi1d 737 . . . . . . . . . . 11 (𝑥 = 𝑣 → ((𝑥 = 𝑦𝑦𝐴) ↔ (𝑣 = 𝑦𝑦𝐴)))
3736exbidv 1837 . . . . . . . . . 10 (𝑥 = 𝑣 → (∃𝑦(𝑥 = 𝑦𝑦𝐴) ↔ ∃𝑦(𝑣 = 𝑦𝑦𝐴)))
3834, 37elab 3319 . . . . . . . . 9 (𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)} ↔ ∃𝑦(𝑣 = 𝑦𝑦𝐴))
3938bicomi 213 . . . . . . . 8 (∃𝑦(𝑣 = 𝑦𝑦𝐴) ↔ 𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)})
4039anbi2i 726 . . . . . . 7 ((𝑧𝑣 ∧ ∃𝑦(𝑣 = 𝑦𝑦𝐴)) ↔ (𝑧𝑣𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)}))
4140exbii 1764 . . . . . 6 (∃𝑣(𝑧𝑣 ∧ ∃𝑦(𝑣 = 𝑦𝑦𝐴)) ↔ ∃𝑣(𝑧𝑣𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)}))
4233, 41bitri 263 . . . . 5 (∃𝑣𝑦(𝑧𝑣 ∧ (𝑣 = 𝑦𝑦𝐴)) ↔ ∃𝑣(𝑧𝑣𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)}))
4331, 32, 423bitri 285 . . . 4 (∃𝑦(𝑦𝐴𝑧 𝑦) ↔ ∃𝑣(𝑧𝑣𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)}))
443, 18, 433bitri 285 . . 3 (∃𝑢(𝑧𝑢𝑢 𝐴) ↔ ∃𝑣(𝑧𝑣𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)}))
4544abbii 2726 . 2 {𝑧 ∣ ∃𝑢(𝑧𝑢𝑢 𝐴)} = {𝑧 ∣ ∃𝑣(𝑧𝑣𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)})}
46 df-uni 4373 . 2 𝐴 = {𝑧 ∣ ∃𝑢(𝑧𝑢𝑢 𝐴)}
47 df-uni 4373 . 2 {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)} = {𝑧 ∣ ∃𝑣(𝑧𝑣𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)})}
4845, 46, 473eqtr4i 2642 1 𝐴 = {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)}
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 383   = wceq 1475  ∃wex 1695   ∈ wcel 1977  {cab 2596  ∪ cuni 4372 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-un 6847 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-v 3175  df-uni 4373 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator