Theorem eliun 3972

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 2812	. 2 |- ( A e. U_ x e. B C -> A e. _V )
2		elex 2812	. . 3 |- ( A e. C -> A e. _V )
3	2	rexlimivw 2644	. 2 |- ( E. x e. B A e. C -> A e. _V )
4		eleq1 2292	. . . 4 |- ( y = A -> ( y e. C <-> A e. C ) )
5	4	rexbidv 2531	. . 3 |- ( y = A -> ( E. x e. B y e. C <-> E. x e. B A e. C ) )
6		df-iun 3970	. . 3 |- U_ x e. B C = { y | E. x e. B y e. C }
7	5, 6	elab2g 2951	. 2 |- ( A e. _V -> ( A e. U_ x e. B C <-> E. x e. B A e. C ) )
8	1, 3, 7	pm5.21nii 709	1 |- ( A e. U_ x e. B C <-> E. x e. B A e. C )

Syntax hints:   <-> wb 105   = wceq 1395   e. wcel 2200   E.wrex 2509   _Vcvv 2800   U_ciun 3968

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2802  df-iun 3970

This theorem is referenced by:  iuncom  3974  iuncom4  3975  iunconstm  3976  iuniin  3978  iunss1  3979  ss2iun  3983  dfiun2g  4000  ssiun  4010  ssiun2  4011  iunab  4015  iun0  4025  0iun  4026  iunn0m  4029  iunin2  4032  iundif2ss  4034  iindif2m  4036  iunxsng  4044  iunxsngf  4046  iunun  4047  iunxun  4048  iunxiun  4050  iunpwss  4060  disjiun  4081  triun  4198  iunpw  4575  xpiundi  4782  xpiundir  4783  iunxpf  4876  cnvuni  4914  dmiun  4938  dmuni  4939  rniun  5145  dfco2  5234  dfco2a  5235  coiun  5244  fun11iun  5601  imaiun  5896  eluniimadm  5901  opabex3d  6278  opabex3  6279  smoiun  6462  tfrlemi14d  6494  tfr1onlemres  6510  tfrcllemres  6523  wrdval  11106  fsum2dlemstep  11985  fisumcom2  11989  fsumiun  12028  fprod2dlemstep  12173  fprodcom2fi  12177  ennnfonelemrn  13030  ennnfonelemdm  13031  ctiunctlemf  13049  ctiunctlemfo  13050  imasaddfnlemg  13387  lssats2  14418  clwwlknun  16236