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

Theorem uniuni 7195
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 4626 . . . . . 6 (𝑢 𝐴 ↔ ∃𝑦(𝑢𝑦𝑦𝐴))
21anbi2i 611 . . . . 5 ((𝑧𝑢𝑢 𝐴) ↔ (𝑧𝑢 ∧ ∃𝑦(𝑢𝑦𝑦𝐴)))
32exbii 1933 . . . 4 (∃𝑢(𝑧𝑢𝑢 𝐴) ↔ ∃𝑢(𝑧𝑢 ∧ ∃𝑦(𝑢𝑦𝑦𝐴)))
4 19.42v 2043 . . . . . . 7 (∃𝑦(𝑧𝑢 ∧ (𝑢𝑦𝑦𝐴)) ↔ (𝑧𝑢 ∧ ∃𝑦(𝑢𝑦𝑦𝐴)))
54bicomi 215 . . . . . 6 ((𝑧𝑢 ∧ ∃𝑦(𝑢𝑦𝑦𝐴)) ↔ ∃𝑦(𝑧𝑢 ∧ (𝑢𝑦𝑦𝐴)))
65exbii 1933 . . . . 5 (∃𝑢(𝑧𝑢 ∧ ∃𝑦(𝑢𝑦𝑦𝐴)) ↔ ∃𝑢𝑦(𝑧𝑢 ∧ (𝑢𝑦𝑦𝐴)))
7 excom 2208 . . . . . 6 (∃𝑢𝑦(𝑧𝑢 ∧ (𝑢𝑦𝑦𝐴)) ↔ ∃𝑦𝑢(𝑧𝑢 ∧ (𝑢𝑦𝑦𝐴)))
8 anass 456 . . . . . . . 8 (((𝑧𝑢𝑢𝑦) ∧ 𝑦𝐴) ↔ (𝑧𝑢 ∧ (𝑢𝑦𝑦𝐴)))
9 ancom 450 . . . . . . . 8 (((𝑧𝑢𝑢𝑦) ∧ 𝑦𝐴) ↔ (𝑦𝐴 ∧ (𝑧𝑢𝑢𝑦)))
108, 9bitr3i 268 . . . . . . 7 ((𝑧𝑢 ∧ (𝑢𝑦𝑦𝐴)) ↔ (𝑦𝐴 ∧ (𝑧𝑢𝑢𝑦)))
11102exbii 1934 . . . . . 6 (∃𝑦𝑢(𝑧𝑢 ∧ (𝑢𝑦𝑦𝐴)) ↔ ∃𝑦𝑢(𝑦𝐴 ∧ (𝑧𝑢𝑢𝑦)))
12 exdistr 2044 . . . . . 6 (∃𝑦𝑢(𝑦𝐴 ∧ (𝑧𝑢𝑢𝑦)) ↔ ∃𝑦(𝑦𝐴 ∧ ∃𝑢(𝑧𝑢𝑢𝑦)))
137, 11, 123bitri 288 . . . . 5 (∃𝑢𝑦(𝑧𝑢 ∧ (𝑢𝑦𝑦𝐴)) ↔ ∃𝑦(𝑦𝐴 ∧ ∃𝑢(𝑧𝑢𝑢𝑦)))
14 eluni 4626 . . . . . . . 8 (𝑧 𝑦 ↔ ∃𝑢(𝑧𝑢𝑢𝑦))
1514bicomi 215 . . . . . . 7 (∃𝑢(𝑧𝑢𝑢𝑦) ↔ 𝑧 𝑦)
1615anbi2i 611 . . . . . 6 ((𝑦𝐴 ∧ ∃𝑢(𝑧𝑢𝑢𝑦)) ↔ (𝑦𝐴𝑧 𝑦))
1716exbii 1933 . . . . 5 (∃𝑦(𝑦𝐴 ∧ ∃𝑢(𝑧𝑢𝑢𝑦)) ↔ ∃𝑦(𝑦𝐴𝑧 𝑦))
186, 13, 173bitri 288 . . . 4 (∃𝑢(𝑧𝑢 ∧ ∃𝑦(𝑢𝑦𝑦𝐴)) ↔ ∃𝑦(𝑦𝐴𝑧 𝑦))
19 vuniex 7178 . . . . . . . . . 10 𝑦 ∈ V
20 eleq2 2870 . . . . . . . . . 10 (𝑣 = 𝑦 → (𝑧𝑣𝑧 𝑦))
2119, 20ceqsexv 3432 . . . . . . . . 9 (∃𝑣(𝑣 = 𝑦𝑧𝑣) ↔ 𝑧 𝑦)
22 exancom 1947 . . . . . . . . 9 (∃𝑣(𝑣 = 𝑦𝑧𝑣) ↔ ∃𝑣(𝑧𝑣𝑣 = 𝑦))
2321, 22bitr3i 268 . . . . . . . 8 (𝑧 𝑦 ↔ ∃𝑣(𝑧𝑣𝑣 = 𝑦))
2423anbi2i 611 . . . . . . 7 ((𝑦𝐴𝑧 𝑦) ↔ (𝑦𝐴 ∧ ∃𝑣(𝑧𝑣𝑣 = 𝑦)))
25 19.42v 2043 . . . . . . 7 (∃𝑣(𝑦𝐴 ∧ (𝑧𝑣𝑣 = 𝑦)) ↔ (𝑦𝐴 ∧ ∃𝑣(𝑧𝑣𝑣 = 𝑦)))
26 ancom 450 . . . . . . . . 9 ((𝑦𝐴 ∧ (𝑧𝑣𝑣 = 𝑦)) ↔ ((𝑧𝑣𝑣 = 𝑦) ∧ 𝑦𝐴))
27 anass 456 . . . . . . . . 9 (((𝑧𝑣𝑣 = 𝑦) ∧ 𝑦𝐴) ↔ (𝑧𝑣 ∧ (𝑣 = 𝑦𝑦𝐴)))
2826, 27bitri 266 . . . . . . . 8 ((𝑦𝐴 ∧ (𝑧𝑣𝑣 = 𝑦)) ↔ (𝑧𝑣 ∧ (𝑣 = 𝑦𝑦𝐴)))
2928exbii 1933 . . . . . . 7 (∃𝑣(𝑦𝐴 ∧ (𝑧𝑣𝑣 = 𝑦)) ↔ ∃𝑣(𝑧𝑣 ∧ (𝑣 = 𝑦𝑦𝐴)))
3024, 25, 293bitr2i 290 . . . . . 6 ((𝑦𝐴𝑧 𝑦) ↔ ∃𝑣(𝑧𝑣 ∧ (𝑣 = 𝑦𝑦𝐴)))
3130exbii 1933 . . . . 5 (∃𝑦(𝑦𝐴𝑧 𝑦) ↔ ∃𝑦𝑣(𝑧𝑣 ∧ (𝑣 = 𝑦𝑦𝐴)))
32 excom 2208 . . . . 5 (∃𝑦𝑣(𝑧𝑣 ∧ (𝑣 = 𝑦𝑦𝐴)) ↔ ∃𝑣𝑦(𝑧𝑣 ∧ (𝑣 = 𝑦𝑦𝐴)))
33 exdistr 2044 . . . . . 6 (∃𝑣𝑦(𝑧𝑣 ∧ (𝑣 = 𝑦𝑦𝐴)) ↔ ∃𝑣(𝑧𝑣 ∧ ∃𝑦(𝑣 = 𝑦𝑦𝐴)))
34 vex 3390 . . . . . . . . . 10 𝑣 ∈ V
35 eqeq1 2806 . . . . . . . . . . . 12 (𝑥 = 𝑣 → (𝑥 = 𝑦𝑣 = 𝑦))
3635anbi1d 617 . . . . . . . . . . 11 (𝑥 = 𝑣 → ((𝑥 = 𝑦𝑦𝐴) ↔ (𝑣 = 𝑦𝑦𝐴)))
3736exbidv 2012 . . . . . . . . . 10 (𝑥 = 𝑣 → (∃𝑦(𝑥 = 𝑦𝑦𝐴) ↔ ∃𝑦(𝑣 = 𝑦𝑦𝐴)))
3834, 37elab 3541 . . . . . . . . 9 (𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)} ↔ ∃𝑦(𝑣 = 𝑦𝑦𝐴))
3938bicomi 215 . . . . . . . 8 (∃𝑦(𝑣 = 𝑦𝑦𝐴) ↔ 𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)})
4039anbi2i 611 . . . . . . 7 ((𝑧𝑣 ∧ ∃𝑦(𝑣 = 𝑦𝑦𝐴)) ↔ (𝑧𝑣𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)}))
4140exbii 1933 . . . . . 6 (∃𝑣(𝑧𝑣 ∧ ∃𝑦(𝑣 = 𝑦𝑦𝐴)) ↔ ∃𝑣(𝑧𝑣𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)}))
4233, 41bitri 266 . . . . 5 (∃𝑣𝑦(𝑧𝑣 ∧ (𝑣 = 𝑦𝑦𝐴)) ↔ ∃𝑣(𝑧𝑣𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)}))
4331, 32, 423bitri 288 . . . 4 (∃𝑦(𝑦𝐴𝑧 𝑦) ↔ ∃𝑣(𝑧𝑣𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)}))
443, 18, 433bitri 288 . . 3 (∃𝑢(𝑧𝑢𝑢 𝐴) ↔ ∃𝑣(𝑧𝑣𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)}))
4544abbii 2919 . 2 {𝑧 ∣ ∃𝑢(𝑧𝑢𝑢 𝐴)} = {𝑧 ∣ ∃𝑣(𝑧𝑣𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)})}
46 df-uni 4624 . 2 𝐴 = {𝑧 ∣ ∃𝑢(𝑧𝑢𝑢 𝐴)}
47 df-uni 4624 . 2 {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)} = {𝑧 ∣ ∃𝑣(𝑧𝑣𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)})}
4845, 46, 473eqtr4i 2834 1 𝐴 = {𝑥 ∣ ∃𝑦(𝑥 = 𝑦𝑦𝐴)}
Colors of variables: wff setvar class
Syntax hints:  wa 384   = wceq 1637  wex 1859  wcel 2155  {cab 2788   cuni 4623
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-8 2157  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781  ax-sep 4968  ax-un 7173
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-rex 3098  df-v 3389  df-uni 4624
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator