Theorem eliun 3690

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 2611	. 2 |- ( A e. U_ x e. B C -> A e. _V )
2		elex 2611	. . 3 |- ( A e. C -> A e. _V )
3	2	rexlimivw 2474	. 2 |- ( E. x e. B A e. C -> A e. _V )
4		eleq1 2142	. . . 4 |- ( y = A -> ( y e. C <-> A e. C ) )
5	4	rexbidv 2370	. . 3 |- ( y = A -> ( E. x e. B y e. C <-> E. x e. B A e. C ) )
6		df-iun 3688	. . 3 |- U_ x e. B C = { y | E. x e. B y e. C }
7	5, 6	elab2g 2741	. 2 |- ( A e. _V -> ( A e. U_ x e. B C <-> E. x e. B A e. C ) )
8	1, 3, 7	pm5.21nii 653	1 |- ( A e. U_ x e. B C <-> E. x e. B A e. C )

Syntax hints:   <-> wb 103   = wceq 1285   e. wcel 1434   E.wrex 2350   _Vcvv 2602   U_ciun 3686

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 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064

This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-ral 2354  df-rex 2355  df-v 2604  df-iun 3688

This theorem is referenced by:  iuncom  3692  iuncom4  3693  iunconstm  3694  iuniin  3696  iunss1  3697  ss2iun  3701  dfiun2g  3718  ssiun  3728  ssiun2  3729  iunab  3732  iun0  3742  0iun  3743  iunn0m  3746  iunin2  3749  iundif2ss  3751  iindif2m  3753  iunxsng  3761  iunun  3763  iunxun  3764  iunxiun  3765  iunpwss  3772  triun  3896  iunpw  4237  xpiundi  4424  xpiundir  4425  iunxpf  4512  cnvuni  4549  dmiun  4572  dmuni  4573  rniun  4764  dfco2  4850  dfco2a  4851  coiun  4860  fun11iun  5178  imaiun  5431  eluniimadm  5436  opabex3d  5779  opabex3  5780  smoiun  5950  tfrlemi14d  5982  tfr1onlemres  5998  tfrcllemres  6011