Theorem eliun 3870

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 2737	. 2 |- ( A e. U_ x e. B C -> A e. _V )
2		elex 2737	. . 3 |- ( A e. C -> A e. _V )
3	2	rexlimivw 2579	. 2 |- ( E. x e. B A e. C -> A e. _V )
4		eleq1 2229	. . . 4 |- ( y = A -> ( y e. C <-> A e. C ) )
5	4	rexbidv 2467	. . 3 |- ( y = A -> ( E. x e. B y e. C <-> E. x e. B A e. C ) )
6		df-iun 3868	. . 3 |- U_ x e. B C = { y | E. x e. B y e. C }
7	5, 6	elab2g 2873	. 2 |- ( A e. _V -> ( A e. U_ x e. B C <-> E. x e. B A e. C ) )
8	1, 3, 7	pm5.21nii 694	1 |- ( A e. U_ x e. B C <-> E. x e. B A e. C )

Syntax hints:   <-> wb 104   = wceq 1343   e. wcel 2136   E.wrex 2445   _Vcvv 2726   U_ciun 3866

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 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-ral 2449  df-rex 2450  df-v 2728  df-iun 3868

This theorem is referenced by:  iuncom  3872  iuncom4  3873  iunconstm  3874  iuniin  3876  iunss1  3877  ss2iun  3881  dfiun2g  3898  ssiun  3908  ssiun2  3909  iunab  3912  iun0  3922  0iun  3923  iunn0m  3926  iunin2  3929  iundif2ss  3931  iindif2m  3933  iunxsng  3941  iunxsngf  3943  iunun  3944  iunxun  3945  iunxiun  3947  iunpwss  3957  disjiun  3977  triun  4093  iunpw  4458  xpiundi  4662  xpiundir  4663  iunxpf  4752  cnvuni  4790  dmiun  4813  dmuni  4814  rniun  5014  dfco2  5103  dfco2a  5104  coiun  5113  fun11iun  5453  imaiun  5728  eluniimadm  5733  opabex3d  6089  opabex3  6090  smoiun  6269  tfrlemi14d  6301  tfr1onlemres  6317  tfrcllemres  6330  fsum2dlemstep  11375  fisumcom2  11379  fsumiun  11418  fprod2dlemstep  11563  fprodcom2fi  11567  ennnfonelemrn  12352  ennnfonelemdm  12353  ctiunctlemf  12371  ctiunctlemfo  12372