Theorem eliun 3979

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 2815	. 2 |- ( A e. U_ x e. B C -> A e. _V )
2		elex 2815	. . 3 |- ( A e. C -> A e. _V )
3	2	rexlimivw 2647	. 2 |- ( E. x e. B A e. C -> A e. _V )
4		eleq1 2294	. . . 4 |- ( y = A -> ( y e. C <-> A e. C ) )
5	4	rexbidv 2534	. . 3 |- ( y = A -> ( E. x e. B y e. C <-> E. x e. B A e. C ) )
6		df-iun 3977	. . 3 |- U_ x e. B C = { y | E. x e. B y e. C }
7	5, 6	elab2g 2954	. 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 2202   E.wrex 2512   _Vcvv 2803   U_ciun 3975

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 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-rex 2517  df-v 2805  df-iun 3977

This theorem is referenced by:  iuncom  3981  iuncom4  3982  iunconstm  3983  iuniin  3985  iunss1  3986  ss2iun  3990  dfiun2g  4007  ssiun  4017  ssiun2  4018  iunab  4022  iun0  4032  0iun  4033  iunn0m  4036  iunin2  4039  iundif2ss  4041  iindif2m  4043  iunxsng  4051  iunxsngf  4053  iunun  4054  iunxun  4055  iunxiun  4057  iunpwss  4067  disjiun  4088  triun  4205  iunpw  4583  xpiundi  4790  xpiundir  4791  iunxpf  4884  cnvuni  4922  dmiun  4946  dmuni  4947  rniun  5154  dfco2  5243  dfco2a  5244  coiun  5253  fun11iun  5613  imaiun  5911  eluniimadm  5916  opabex3d  6292  opabex3  6293  smoiun  6510  tfrlemi14d  6542  tfr1onlemres  6558  tfrcllemres  6571  wrdval  11165  fsum2dlemstep  12058  fisumcom2  12062  fsumiun  12101  fprod2dlemstep  12246  fprodcom2fi  12250  ennnfonelemrn  13103  ennnfonelemdm  13104  ctiunctlemf  13122  ctiunctlemfo  13123  imasaddfnlemg  13460  lssats2  14493  clwwlknun  16365