Theorem eliun 3682

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 2610	. 2 |- ( A e. U_ x e. B C -> A e. _V )
2		elex 2610	. . 3 |- ( A e. C -> A e. _V )
3	2	rexlimivw 2473	. 2 |- ( E. x e. B A e. C -> A e. _V )
4		eleq1 2141	. . . 4 |- ( y = A -> ( y e. C <-> A e. C ) )
5	4	rexbidv 2369	. . 3 |- ( y = A -> ( E. x e. B y e. C <-> E. x e. B A e. C ) )
6		df-iun 3680	. . 3 |- U_ x e. B C = { y | E. x e. B y e. C }
7	5, 6	elab2g 2740	. 2 |- ( A e. _V -> ( A e. U_ x e. B C <-> E. x e. B A e. C ) )
8	1, 3, 7	pm5.21nii 652	1 |- ( A e. U_ x e. B C <-> E. x e. B A e. C )

Syntax hints:   <-> wb 103   = wceq 1284   e. wcel 1433   E.wrex 2349   _Vcvv 2601   U_ciun 3678

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-ral 2353  df-rex 2354  df-v 2603  df-iun 3680

This theorem is referenced by:  iuncom  3684  iuncom4  3685  iunconstm  3686  iuniin  3688  iunss1  3689  ss2iun  3693  dfiun2g  3710  ssiun  3720  ssiun2  3721  iunab  3724  iun0  3734  0iun  3735  iunn0m  3738  iunin2  3741  iundif2ss  3743  iindif2m  3745  iunxsng  3753  iunun  3755  iunxun  3756  iunxiun  3757  iunpwss  3764  triun  3888  iunpw  4229  xpiundi  4416  xpiundir  4417  iunxpf  4502  cnvuni  4539  dmiun  4562  dmuni  4563  rniun  4754  dfco2  4840  dfco2a  4841  coiun  4850  fun11iun  5167  imaiun  5420  eluniimadm  5425  opabex3d  5768  opabex3  5769  smoiun  5939  tfrlemi14d  5970