Theorem eliun 3974

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 2814	. 2 |- ( A e. U_ x e. B C -> A e. _V )
2		elex 2814	. . 3 |- ( A e. C -> A e. _V )
3	2	rexlimivw 2646	. 2 |- ( E. x e. B A e. C -> A e. _V )
4		eleq1 2294	. . . 4 |- ( y = A -> ( y e. C <-> A e. C ) )
5	4	rexbidv 2533	. . 3 |- ( y = A -> ( E. x e. B y e. C <-> E. x e. B A e. C ) )
6		df-iun 3972	. . 3 |- U_ x e. B C = { y | E. x e. B y e. C }
7	5, 6	elab2g 2953	. 2 |- ( A e. _V -> ( A e. U_ x e. B C <-> E. x e. B A e. C ) )
8	1, 3, 7	pm5.21nii 711	1 |- ( A e. U_ x e. B C <-> E. x e. B A e. C )

Syntax hints:   <-> wb 105   = wceq 1397   e. wcel 2202   E.wrex 2511   _Vcvv 2802   U_ciun 3970

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-v 2804  df-iun 3972

This theorem is referenced by:  iuncom  3976  iuncom4  3977  iunconstm  3978  iuniin  3980  iunss1  3981  ss2iun  3985  dfiun2g  4002  ssiun  4012  ssiun2  4013  iunab  4017  iun0  4027  0iun  4028  iunn0m  4031  iunin2  4034  iundif2ss  4036  iindif2m  4038  iunxsng  4046  iunxsngf  4048  iunun  4049  iunxun  4050  iunxiun  4052  iunpwss  4062  disjiun  4083  triun  4200  iunpw  4577  xpiundi  4784  xpiundir  4785  iunxpf  4878  cnvuni  4916  dmiun  4940  dmuni  4941  rniun  5147  dfco2  5236  dfco2a  5237  coiun  5246  fun11iun  5604  imaiun  5900  eluniimadm  5905  opabex3d  6282  opabex3  6283  smoiun  6466  tfrlemi14d  6498  tfr1onlemres  6514  tfrcllemres  6527  wrdval  11115  fsum2dlemstep  11994  fisumcom2  11998  fsumiun  12037  fprod2dlemstep  12182  fprodcom2fi  12186  ennnfonelemrn  13039  ennnfonelemdm  13040  ctiunctlemf  13058  ctiunctlemfo  13059  imasaddfnlemg  13396  lssats2  14427  clwwlknun  16291