Theorem eliun 4011

Description: Membership in indexed union. (Contributed by NM, 3-Sep-2003.)

Assertion

Ref	Expression
eliun	|- ( A e. U_ x e. B C <-> E. x e. B A e. C )

Distinct variable group:   x, A

Allowed substitution hints:   B( x)   C( x)

Proof of Theorem eliun

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 2833	. 2 |- ( A e. U_ x e. B C -> A e. _V )
2		elex 2833	. . 3 |- ( A e. C -> A e. _V )
3	2	rexlimivw 2664	. 2 |- ( E. x e. B A e. C -> A e. _V )
4		eleq1 2301	. . . 4 |- ( y = A -> ( y e. C <-> A e. C ) )
5	4	rexbidv 2551	. . 3 |- ( y = A -> ( E. x e. B y e. C <-> E. x e. B A e. C ) )
6		df-iun 4009	. . 3 |- U_ x e. B C = { y | E. x e. B y e. C }
7	5, 6	elab2g 2973	. 2 |- ( A e. _V -> ( A e. U_ x e. B C <-> E. x e. B A e. C ) )
8	1, 3, 7	pm5.21nii 716	1 |- ( A e. U_ x e. B C <-> E. x e. B A e. C )

Syntax hints:   <-> wb 105   = wceq 1402   e. wcel 2209   E.wrex 2529   _Vcvv 2821   U_ciun 4007

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-v 2823  df-iun 4009

This theorem is referenced by:  iuncom  4013  iuncom4  4014  iunconstm  4015  iuniin  4017  iunss1  4018  ss2iun  4022  dfiun2g  4039  ssiun  4049  ssiun2  4050  iunab  4054  iun0  4064  0iun  4065  iunn0m  4068  iunin2  4071  iundif2ss  4073  iindif2m  4075  iunxsng  4083  iunxsngf  4085  iunun  4086  iunxun  4087  iunxiun  4089  iunpwss  4099  disjiun  4120  triun  4237  iunpw  4621  xpiundi  4828  xpiundir  4829  iunxpf  4923  cnvuni  4961  dmiun  4985  dmuni  4986  rniun  5193  dfco2  5282  dfco2a  5283  coiun  5292  fun11iun  5655  imaiun  5956  eluniimadm  5961  opabex3d  6340  opabex3  6341  smoiun  6562  tfrlemi14d  6594  tfr1onlemres  6610  tfrcllemres  6623  wrdval  11285  fsum2dlemstep  12179  fisumcom2  12183  fsumiun  12222  fprod2dlemstep  12367  fprodcom2fi  12371  ennnfonelemrn  13288  ennnfonelemdm  13289  ctiunctlemf  13307  ctiunctlemfo  13308  imasaddfnlemg  13612  lssats2  14723  clwwlknun  16596