Theorem eliun 3995

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 2825	. 2 |- ( A e. U_ x e. B C -> A e. _V )
2		elex 2825	. . 3 |- ( A e. C -> A e. _V )
3	2	rexlimivw 2656	. 2 |- ( E. x e. B A e. C -> A e. _V )
4		eleq1 2295	. . . 4 |- ( y = A -> ( y e. C <-> A e. C ) )
5	4	rexbidv 2543	. . 3 |- ( y = A -> ( E. x e. B y e. C <-> E. x e. B A e. C ) )
6		df-iun 3993	. . 3 |- U_ x e. B C = { y | E. x e. B y e. C }
7	5, 6	elab2g 2964	. 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 2203   E.wrex 2521   _Vcvv 2813   U_ciun 3991

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 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-v 2815  df-iun 3993

This theorem is referenced by:  iuncom  3997  iuncom4  3998  iunconstm  3999  iuniin  4001  iunss1  4002  ss2iun  4006  dfiun2g  4023  ssiun  4033  ssiun2  4034  iunab  4038  iun0  4048  0iun  4049  iunn0m  4052  iunin2  4055  iundif2ss  4057  iindif2m  4059  iunxsng  4067  iunxsngf  4069  iunun  4070  iunxun  4071  iunxiun  4073  iunpwss  4083  disjiun  4104  triun  4221  iunpw  4601  xpiundi  4808  xpiundir  4809  iunxpf  4903  cnvuni  4941  dmiun  4965  dmuni  4966  rniun  5173  dfco2  5262  dfco2a  5263  coiun  5272  fun11iun  5635  imaiun  5933  eluniimadm  5938  opabex3d  6314  opabex3  6315  smoiun  6532  tfrlemi14d  6564  tfr1onlemres  6580  tfrcllemres  6593  wrdval  11227  fsum2dlemstep  12120  fisumcom2  12124  fsumiun  12163  fprod2dlemstep  12308  fprodcom2fi  12312  ennnfonelemrn  13170  ennnfonelemdm  13171  ctiunctlemf  13189  ctiunctlemfo  13190  imasaddfnlemg  13527  lssats2  14562  clwwlknun  16436