Theorem eliun 3652

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 2560	. 2 |- (A e. U_x e. B C -> A e. _V)
2		elex 2560	. . 3 |- (A e. C -> A e. _V)
3	2	rexlimivw 2423	. 2 |- (E.x e. B A e. C -> A e. _V)
4		eleq1 2097	. . . 4 |- (y = A -> (y e. C <-> A e. C))
5	4	rexbidv 2321	. . 3 |- (y = A -> (E.x e. B y e. C <-> E.x e. B A e. C))
6		df-iun 3650	. . 3 |- U_x e. B C = {y | E.x e. B y e. C }
7	5, 6	elab2g 2683	. 2 |- (A e. _V -> (A e. U_x e. B C <-> E.x e. B A e. C))
8	1, 3, 7	pm5.21nii 619	1 |- (A e. U_x e. B C <-> E.x e. B A e. C)

Syntax hints:   <-> wb 98   = wceq 1242   e. wcel 1390  E.wrex 2301   _Vcvv 2551   U_ciun 3648

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 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-iun 3650

This theorem is referenced by:  iuncom  3654  iuncom4  3655  iunconstm  3656  iuniin  3658  iunss1  3659  ss2iun  3663  dfiun2g  3680  ssiun  3690  ssiun2  3691  iunab  3694  iun0  3704  0iun  3705  iunn0m  3708  iunin2  3711  iundif2ss  3713  iindif2m  3715  iunxsng  3723  iunun  3725  iunxun  3726  iunxiun  3727  iunpwss  3734  triun  3858  iunpw  4177  xpiundi  4341  xpiundir  4342  iunxpf  4427  cnvuni  4464  dmiun  4487  dmuni  4488  rniun  4677  dfco2  4763  dfco2a  4764  coiun  4773  fun11iun  5090  imaiun  5342  eluniimadm  5347  opabex3d  5690  opabex3  5691  smoiun  5857  tfrlemi14d  5888