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

Theorem uniuni 4133
Description: Expression for double union that moves union into a class builder. (Contributed by FL, 28-May-2007.)
Assertion
Ref Expression
uniuni A = {xy(x = y y A)}
Distinct variable group:   x,A,y

Proof of Theorem uniuni
Dummy variables v z u are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eluni 3557 . . . . . 6 (u Ay(u y y A))
21anbi2i 433 . . . . 5 ((z u u A) ↔ (z u y(u y y A)))
32exbii 1478 . . . 4 (u(z u u A) ↔ u(z u y(u y y A)))
4 19.42v 1768 . . . . . . 7 (y(z u (u y y A)) ↔ (z u y(u y y A)))
54bicomi 123 . . . . . 6 ((z u y(u y y A)) ↔ y(z u (u y y A)))
65exbii 1478 . . . . 5 (u(z u y(u y y A)) ↔ uy(z u (u y y A)))
7 excom 1536 . . . . . 6 (uy(z u (u y y A)) ↔ yu(z u (u y y A)))
8 anass 383 . . . . . . . 8 (((z u u y) y A) ↔ (z u (u y y A)))
9 ancom 253 . . . . . . . 8 (((z u u y) y A) ↔ (y A (z u u y)))
108, 9bitr3i 175 . . . . . . 7 ((z u (u y y A)) ↔ (y A (z u u y)))
11102exbii 1479 . . . . . 6 (yu(z u (u y y A)) ↔ yu(y A (z u u y)))
12 exdistr 1769 . . . . . 6 (yu(y A (z u u y)) ↔ y(y A u(z u u y)))
137, 11, 123bitri 195 . . . . 5 (uy(z u (u y y A)) ↔ y(y A u(z u u y)))
14 eluni 3557 . . . . . . . 8 (z yu(z u u y))
1514bicomi 123 . . . . . . 7 (u(z u u y) ↔ z y)
1615anbi2i 433 . . . . . 6 ((y A u(z u u y)) ↔ (y A z y))
1716exbii 1478 . . . . 5 (y(y A u(z u u y)) ↔ y(y A z y))
186, 13, 173bitri 195 . . . 4 (u(z u y(u y y A)) ↔ y(y A z y))
19 vex 2538 . . . . . . . . . . 11 y V
2019uniex 4124 . . . . . . . . . 10 y V
21 eleq2 2083 . . . . . . . . . 10 (v = y → (z vz y))
2220, 21ceqsexv 2570 . . . . . . . . 9 (v(v = y z v) ↔ z y)
23 exancom 1481 . . . . . . . . 9 (v(v = y z v) ↔ v(z v v = y))
2422, 23bitr3i 175 . . . . . . . 8 (z yv(z v v = y))
2524anbi2i 433 . . . . . . 7 ((y A z y) ↔ (y A v(z v v = y)))
26 19.42v 1768 . . . . . . 7 (v(y A (z v v = y)) ↔ (y A v(z v v = y)))
27 ancom 253 . . . . . . . . 9 ((y A (z v v = y)) ↔ ((z v v = y) y A))
28 anass 383 . . . . . . . . 9 (((z v v = y) y A) ↔ (z v (v = y y A)))
2927, 28bitri 173 . . . . . . . 8 ((y A (z v v = y)) ↔ (z v (v = y y A)))
3029exbii 1478 . . . . . . 7 (v(y A (z v v = y)) ↔ v(z v (v = y y A)))
3125, 26, 303bitr2i 197 . . . . . 6 ((y A z y) ↔ v(z v (v = y y A)))
3231exbii 1478 . . . . 5 (y(y A z y) ↔ yv(z v (v = y y A)))
33 excom 1536 . . . . 5 (yv(z v (v = y y A)) ↔ vy(z v (v = y y A)))
34 exdistr 1769 . . . . . 6 (vy(z v (v = y y A)) ↔ v(z v y(v = y y A)))
35 vex 2538 . . . . . . . . . 10 v V
36 eqeq1 2028 . . . . . . . . . . . 12 (x = v → (x = yv = y))
3736anbi1d 441 . . . . . . . . . . 11 (x = v → ((x = y y A) ↔ (v = y y A)))
3837exbidv 1688 . . . . . . . . . 10 (x = v → (y(x = y y A) ↔ y(v = y y A)))
3935, 38elab 2664 . . . . . . . . 9 (v {xy(x = y y A)} ↔ y(v = y y A))
4039bicomi 123 . . . . . . . 8 (y(v = y y A) ↔ v {xy(x = y y A)})
4140anbi2i 433 . . . . . . 7 ((z v y(v = y y A)) ↔ (z v v {xy(x = y y A)}))
4241exbii 1478 . . . . . 6 (v(z v y(v = y y A)) ↔ v(z v v {xy(x = y y A)}))
4334, 42bitri 173 . . . . 5 (vy(z v (v = y y A)) ↔ v(z v v {xy(x = y y A)}))
4432, 33, 433bitri 195 . . . 4 (y(y A z y) ↔ v(z v v {xy(x = y y A)}))
453, 18, 443bitri 195 . . 3 (u(z u u A) ↔ v(z v v {xy(x = y y A)}))
4645abbii 2135 . 2 {zu(z u u A)} = {zv(z v v {xy(x = y y A)})}
47 df-uni 3555 . 2 A = {zu(z u u A)}
48 df-uni 3555 . 2 {xy(x = y y A)} = {zv(z v v {xy(x = y y A)})}
4946, 47, 483eqtr4i 2052 1 A = {xy(x = y y A)}
Colors of variables: wff set class
Syntax hints:   wa 97   = wceq 1228  wex 1362   wcel 1374  {cab 2008   cuni 3554
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 617  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-10 1377  ax-11 1378  ax-i12 1379  ax-bnd 1380  ax-4 1381  ax-13 1385  ax-14 1386  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410  ax-ext 2004  ax-sep 3849  ax-un 4120
This theorem depends on definitions:  df-bi 110  df-tru 1231  df-nf 1330  df-sb 1628  df-clab 2009  df-cleq 2015  df-clel 2018  df-nfc 2149  df-rex 2290  df-v 2537  df-uni 3555
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator