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

Theorem uniuni 4708
 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 4010 . . . . . 6
21anbi2i 676 . . . . 5
32exbii 1592 . . . 4
4 19.42v 1928 . . . . . . 7
54bicomi 194 . . . . . 6
65exbii 1592 . . . . 5
7 excom 1756 . . . . . 6
8 anass 631 . . . . . . . 8
9 ancom 438 . . . . . . . 8
108, 9bitr3i 243 . . . . . . 7
11102exbii 1593 . . . . . 6
12 exdistr 1929 . . . . . 6
137, 11, 123bitri 263 . . . . 5
14 eluni 4010 . . . . . . . 8
1514bicomi 194 . . . . . . 7
1615anbi2i 676 . . . . . 6
1716exbii 1592 . . . . 5
186, 13, 173bitri 263 . . . 4
19 vex 2951 . . . . . . . . . . 11
2019uniex 4697 . . . . . . . . . 10
21 eleq2 2496 . . . . . . . . . 10
2220, 21ceqsexv 2983 . . . . . . . . 9
23 exancom 1596 . . . . . . . . 9
2422, 23bitr3i 243 . . . . . . . 8
2524anbi2i 676 . . . . . . 7
26 19.42v 1928 . . . . . . 7
27 ancom 438 . . . . . . . . 9
28 anass 631 . . . . . . . . 9
2927, 28bitri 241 . . . . . . . 8
3029exbii 1592 . . . . . . 7
3125, 26, 303bitr2i 265 . . . . . 6
3231exbii 1592 . . . . 5
33 excom 1756 . . . . 5
34 exdistr 1929 . . . . . 6
35 vex 2951 . . . . . . . . . 10
36 eqeq1 2441 . . . . . . . . . . . 12
3736anbi1d 686 . . . . . . . . . . 11
3837exbidv 1636 . . . . . . . . . 10
3935, 38elab 3074 . . . . . . . . 9
4039bicomi 194 . . . . . . . 8
4140anbi2i 676 . . . . . . 7
4241exbii 1592 . . . . . 6
4334, 42bitri 241 . . . . 5
4432, 33, 433bitri 263 . . . 4
453, 18, 443bitri 263 . . 3
4645abbii 2547 . 2
47 df-uni 4008 . 2
48 df-uni 4008 . 2
4946, 47, 483eqtr4i 2465 1
 Colors of variables: wff set class Syntax hints:   wa 359  wex 1550   wceq 1652   wcel 1725  cab 2421  cuni 4007 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-un 4693 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rex 2703  df-v 2950  df-uni 4008
 Copyright terms: Public domain W3C validator