Theorem eliun 3661

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 2566	. 2 |- ( A e. U_ x e. B C -> A e. _V )
2		elex 2566	. . 3 |- ( A e. C -> A e. _V )
3	2	rexlimivw 2429	. 2 |- ( E. x e. B A e. C -> A e. _V )
4		eleq1 2100	. . . 4 |- ( y = A -> ( y e. C <-> A e. C ) )
5	4	rexbidv 2327	. . 3 |- ( y = A -> ( E. x e. B y e. C <-> E. x e. B A e. C ) )
6		df-iun 3659	. . 3 |- U_ x e. B C = { y | E. x e. B y e. C }
7	5, 6	elab2g 2689	. 2 |- ( A e. _V -> ( A e. U_ x e. B C <-> E. x e. B A e. C ) )
8	1, 3, 7	pm5.21nii 620	1 |- ( A e. U_ x e. B C <-> E. x e. B A e. C )

Syntax hints:   <-> wb 98   = wceq 1243   e. wcel 1393   E.wrex 2307   _Vcvv 2557   U_ciun 3657

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ral 2311  df-rex 2312  df-v 2559  df-iun 3659

This theorem is referenced by:  iuncom  3663  iuncom4  3664  iunconstm  3665  iuniin  3667  iunss1  3668  ss2iun  3672  dfiun2g  3689  ssiun  3699  ssiun2  3700  iunab  3703  iun0  3713  0iun  3714  iunn0m  3717  iunin2  3720  iundif2ss  3722  iindif2m  3724  iunxsng  3732  iunun  3734  iunxun  3735  iunxiun  3736  iunpwss  3743  triun  3867  iunpw  4211  xpiundi  4398  xpiundir  4399  iunxpf  4484  cnvuni  4521  dmiun  4544  dmuni  4545  rniun  4734  dfco2  4820  dfco2a  4821  coiun  4830  fun11iun  5147  imaiun  5399  eluniimadm  5404  opabex3d  5748  opabex3  5749  smoiun  5916  tfrlemi14d  5947