Theorem eliun 4000

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 2827	. 2 |- ( A e. U_ x e. B C -> A e. _V )
2		elex 2827	. . 3 |- ( A e. C -> A e. _V )
3	2	rexlimivw 2658	. 2 |- ( E. x e. B A e. C -> A e. _V )
4		eleq1 2297	. . . 4 |- ( y = A -> ( y e. C <-> A e. C ) )
5	4	rexbidv 2545	. . 3 |- ( y = A -> ( E. x e. B y e. C <-> E. x e. B A e. C ) )
6		df-iun 3998	. . 3 |- U_ x e. B C = { y | E. x e. B y e. C }
7	5, 6	elab2g 2967	. 2 |- ( A e. _V -> ( A e. U_ x e. B C <-> E. x e. B A e. C ) )
8	1, 3, 7	pm5.21nii 712	1 |- ( A e. U_ x e. B C <-> E. x e. B A e. C )

Syntax hints:   <-> wb 105   = wceq 1398   e. wcel 2205   E.wrex 2523   _Vcvv 2815   U_ciun 3996

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-rex 2528  df-v 2817  df-iun 3998

This theorem is referenced by:  iuncom  4002  iuncom4  4003  iunconstm  4004  iuniin  4006  iunss1  4007  ss2iun  4011  dfiun2g  4028  ssiun  4038  ssiun2  4039  iunab  4043  iun0  4053  0iun  4054  iunn0m  4057  iunin2  4060  iundif2ss  4062  iindif2m  4064  iunxsng  4072  iunxsngf  4074  iunun  4075  iunxun  4076  iunxiun  4078  iunpwss  4088  disjiun  4109  triun  4226  iunpw  4606  xpiundi  4813  xpiundir  4814  iunxpf  4908  cnvuni  4946  dmiun  4970  dmuni  4971  rniun  5178  dfco2  5267  dfco2a  5268  coiun  5277  fun11iun  5640  imaiun  5939  eluniimadm  5944  opabex3d  6323  opabex3  6324  smoiun  6545  tfrlemi14d  6577  tfr1onlemres  6593  tfrcllemres  6606  wrdval  11252  fsum2dlemstep  12145  fisumcom2  12149  fsumiun  12188  fprod2dlemstep  12333  fprodcom2fi  12337  ennnfonelemrn  13254  ennnfonelemdm  13255  ctiunctlemf  13273  ctiunctlemfo  13274  imasaddfnlemg  13578  lssats2  14688  clwwlknun  16562