Theorem eliun 3890

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 2748	. 2 |- ( A e. U_ x e. B C -> A e. _V )
2		elex 2748	. . 3 |- ( A e. C -> A e. _V )
3	2	rexlimivw 2590	. 2 |- ( E. x e. B A e. C -> A e. _V )
4		eleq1 2240	. . . 4 |- ( y = A -> ( y e. C <-> A e. C ) )
5	4	rexbidv 2478	. . 3 |- ( y = A -> ( E. x e. B y e. C <-> E. x e. B A e. C ) )
6		df-iun 3888	. . 3 |- U_ x e. B C = { y | E. x e. B y e. C }
7	5, 6	elab2g 2884	. 2 |- ( A e. _V -> ( A e. U_ x e. B C <-> E. x e. B A e. C ) )
8	1, 3, 7	pm5.21nii 704	1 |- ( A e. U_ x e. B C <-> E. x e. B A e. C )

Syntax hints:   <-> wb 105   = wceq 1353   e. wcel 2148   E.wrex 2456   _Vcvv 2737   U_ciun 3886

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2739  df-iun 3888

This theorem is referenced by:  iuncom  3892  iuncom4  3893  iunconstm  3894  iuniin  3896  iunss1  3897  ss2iun  3901  dfiun2g  3918  ssiun  3928  ssiun2  3929  iunab  3933  iun0  3943  0iun  3944  iunn0m  3947  iunin2  3950  iundif2ss  3952  iindif2m  3954  iunxsng  3962  iunxsngf  3964  iunun  3965  iunxun  3966  iunxiun  3968  iunpwss  3978  disjiun  3998  triun  4114  iunpw  4480  xpiundi  4684  xpiundir  4685  iunxpf  4775  cnvuni  4813  dmiun  4836  dmuni  4837  rniun  5039  dfco2  5128  dfco2a  5129  coiun  5138  fun11iun  5482  imaiun  5760  eluniimadm  5765  opabex3d  6121  opabex3  6122  smoiun  6301  tfrlemi14d  6333  tfr1onlemres  6349  tfrcllemres  6362  fsum2dlemstep  11441  fisumcom2  11445  fsumiun  11484  fprod2dlemstep  11629  fprodcom2fi  11633  ennnfonelemrn  12419  ennnfonelemdm  12420  ctiunctlemf  12438  ctiunctlemfo  12439  imasaddfnlemg  12734