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

Theorem iunpw 6605
 Description: An indexed union of a power class in terms of the power class of the union of its index. Part of Exercise 24(b) of [Enderton] p. 33. (Contributed by NM, 29-Nov-2003.)
Hypothesis
Ref Expression
iunpw.1
Assertion
Ref Expression
iunpw
Distinct variable group:   ,

Proof of Theorem iunpw
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 sseq2 3454 . . . . . . . 8
21biimprcd 229 . . . . . . 7
32reximdv 2861 . . . . . 6
43com12 32 . . . . 5
5 ssiun 4320 . . . . . 6
6 uniiun 4331 . . . . . 6
75, 6syl6sseqr 3479 . . . . 5
84, 7impbid1 207 . . . 4
9 selpw 3958 . . . 4
10 eliun 4283 . . . . 5
11 selpw 3958 . . . . . 6
1211rexbii 2889 . . . . 5
1310, 12bitri 253 . . . 4
148, 9, 133bitr4g 292 . . 3
1514eqrdv 2449 . 2
16 ssid 3451 . . . . 5
17 iunpw.1 . . . . . . . 8
1817uniex 6587 . . . . . . 7
1918elpw 3957 . . . . . 6
20 eleq2 2518 . . . . . 6
2119, 20syl5bbr 263 . . . . 5
2216, 21mpbii 215 . . . 4
23 eliun 4283 . . . 4
2422, 23sylib 200 . . 3
25 elssuni 4227 . . . . . . 7
26 elpwi 3960 . . . . . . 7
2725, 26anim12i 570 . . . . . 6
28 eqss 3447 . . . . . 6
2927, 28sylibr 216 . . . . 5
3029ex 436 . . . 4
3130reximia 2853 . . 3
3224, 31syl 17 . 2
3315, 32impbii 191 1
 Colors of variables: wff setvar class Syntax hints:   wb 188   wa 371   wceq 1444   wcel 1887  wrex 2738  cvv 3045   wss 3404  cpw 3951  cuni 4198  ciun 4278 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-un 6583 This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ral 2742  df-rex 2743  df-v 3047  df-in 3411  df-ss 3418  df-pw 3953  df-uni 4199  df-iun 4280 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator