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

Theorem iunexg 6757
Description: The existence of an indexed union.  x is normally a free-variable parameter in  B. (Contributed by NM, 23-Mar-2006.)
Assertion
Ref Expression
iunexg  |-  ( ( A  e.  V  /\  A. x  e.  A  B  e.  W )  ->  U_ x  e.  A  B  e.  _V )
Distinct variable group:    x, A
Allowed substitution hints:    B( x)    V( x)    W( x)

Proof of Theorem iunexg
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 dfiun2g 4280 . . 3  |-  ( A. x  e.  A  B  e.  W  ->  U_ x  e.  A  B  =  U. { y  |  E. x  e.  A  y  =  B } )
21adantl 472 . 2  |-  ( ( A  e.  V  /\  A. x  e.  A  B  e.  W )  ->  U_ x  e.  A  B  =  U. { y  |  E. x  e.  A  y  =  B } )
3 abrexexg 6756 . . . 4  |-  ( A  e.  V  ->  { y  |  E. x  e.  A  y  =  B }  e.  _V )
4 uniexg 6576 . . . 4  |-  ( { y  |  E. x  e.  A  y  =  B }  e.  _V  ->  U. { y  |  E. x  e.  A  y  =  B }  e.  _V )
53, 4syl 17 . . 3  |-  ( A  e.  V  ->  U. {
y  |  E. x  e.  A  y  =  B }  e.  _V )
65adantr 471 . 2  |-  ( ( A  e.  V  /\  A. x  e.  A  B  e.  W )  ->  U. {
y  |  E. x  e.  A  y  =  B }  e.  _V )
72, 6eqeltrd 2530 1  |-  ( ( A  e.  V  /\  A. x  e.  A  B  e.  W )  ->  U_ x  e.  A  B  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    = wceq 1448    e. wcel 1891   {cab 2438   A.wral 2737   E.wrex 2738   _Vcvv 3013   U.cuni 4168   U_ciun 4248
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-8 1893  ax-9 1900  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432  ax-rep 4487  ax-sep 4497  ax-nul 4506  ax-pr 4612  ax-un 6571
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 988  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-eu 2304  df-mo 2305  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-ne 2624  df-ral 2742  df-rex 2743  df-reu 2744  df-rab 2746  df-v 3015  df-sbc 3236  df-csb 3332  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-nul 3700  df-if 3850  df-sn 3937  df-pr 3939  df-op 3943  df-uni 4169  df-iun 4250  df-br 4375  df-opab 4434  df-mpt 4435  df-id 4727  df-xp 4818  df-rel 4819  df-cnv 4820  df-co 4821  df-dm 4822  df-rn 4823  df-res 4824  df-ima 4825  df-iota 5525  df-fun 5563  df-fn 5564  df-f 5565  df-f1 5566  df-fo 5567  df-f1o 5568  df-fv 5569
This theorem is referenced by:  abrexex2g  6758  opabex3d  6759  opabex3  6760  iunex  6761  xpexgALT  6774  mpt2exxg  6855  ixpexg  7533  ixpssmapg  7539  iundom  8954  iunctb  8986  cshwsex  15082  imasplusg  15429  imasmulr  15430  imasvsca  15432  imasip  15433  gsum2d2  17617  gsumcom2  17618  dprd2da  17686  ptcls  20642  ptcmplem2  21079  elpwiuncl  28167  aciunf1lem  28272  esum2dlem  28920  esum2d  28921  esumiun  28922  omssubadd  29134  omssubaddOLD  29138  eulerpartlemgs2  29219  bnj535  29707  bnj546  29713  bnj893  29745  bnj1136  29812  bnj1413  29850  trpredtr  30477  trpredmintr  30478  trpredrec  30485  eliunov2  36273  fvmptiunrelexplb0d  36278  fvmptiunrelexplb1d  36280  iunrelexp0  36296  unirnmapsn  37508  iunmapss  37509  ssmapsn  37510  iunmapsn  37511  sge0iunmptlemfi  38314  sge0iunmpt  38319  mpt2exxg2  40444
  Copyright terms: Public domain W3C validator