Theorem eliun 3877

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 2741	. 2 |- ( A e. U_ x e. B C -> A e. _V )
2		elex 2741	. . 3 |- ( A e. C -> A e. _V )
3	2	rexlimivw 2583	. 2 |- ( E. x e. B A e. C -> A e. _V )
4		eleq1 2233	. . . 4 |- ( y = A -> ( y e. C <-> A e. C ) )
5	4	rexbidv 2471	. . 3 |- ( y = A -> ( E. x e. B y e. C <-> E. x e. B A e. C ) )
6		df-iun 3875	. . 3 |- U_ x e. B C = { y | E. x e. B y e. C }
7	5, 6	elab2g 2877	. 2 |- ( A e. _V -> ( A e. U_ x e. B C <-> E. x e. B A e. C ) )
8	1, 3, 7	pm5.21nii 699	1 |- ( A e. U_ x e. B C <-> E. x e. B A e. C )

Syntax hints:   <-> wb 104   = wceq 1348   e. wcel 2141   E.wrex 2449   _Vcvv 2730   U_ciun 3873

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453  df-rex 2454  df-v 2732  df-iun 3875

This theorem is referenced by:  iuncom  3879  iuncom4  3880  iunconstm  3881  iuniin  3883  iunss1  3884  ss2iun  3888  dfiun2g  3905  ssiun  3915  ssiun2  3916  iunab  3919  iun0  3929  0iun  3930  iunn0m  3933  iunin2  3936  iundif2ss  3938  iindif2m  3940  iunxsng  3948  iunxsngf  3950  iunun  3951  iunxun  3952  iunxiun  3954  iunpwss  3964  disjiun  3984  triun  4100  iunpw  4465  xpiundi  4669  xpiundir  4670  iunxpf  4759  cnvuni  4797  dmiun  4820  dmuni  4821  rniun  5021  dfco2  5110  dfco2a  5111  coiun  5120  fun11iun  5463  imaiun  5739  eluniimadm  5744  opabex3d  6100  opabex3  6101  smoiun  6280  tfrlemi14d  6312  tfr1onlemres  6328  tfrcllemres  6341  fsum2dlemstep  11397  fisumcom2  11401  fsumiun  11440  fprod2dlemstep  11585  fprodcom2fi  11589  ennnfonelemrn  12374  ennnfonelemdm  12375  ctiunctlemf  12393  ctiunctlemfo  12394