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.

Step	Hyp	Ref	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 } )
2	1	adantl 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 )
5	3, 4	syl 17	. . 3 |- ( A e. V -> U. { y | E. x e. A y = B } e. _V )
6	5	adantr 471	. 2 |- ( ( A e. V /\ A. x e. A B e. W ) -> U. { y | E. x e. A y = B } e. _V )
7	2, 6	eqeltrd 2530	1 |- ( ( A e. V /\ A. x e. A B e. W ) -> U_ x e. A B e. _V )

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