Theorem eliun 3973

Description: Membership in indexed union. (Contributed by NM, 3-Sep-2003.)

Assertion

Ref	Expression
eliun	⊢ (A ∈ ∪x ∈ B C ↔ ∃x ∈ B A ∈ 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 2867	. 2 ⊢ (A ∈ ∪x ∈ B C → A ∈ V)
2		elex 2867	. . 3 ⊢ (A ∈ C → A ∈ V)
3	2	rexlimivw 2734	. 2 ⊢ (∃x ∈ B A ∈ C → A ∈ V)
4		eleq1 2413	. . . 4 ⊢ (y = A → (y ∈ C ↔ A ∈ C))
5	4	rexbidv 2635	. . 3 ⊢ (y = A → (∃x ∈ B y ∈ C ↔ ∃x ∈ B A ∈ C))
6		df-iun 3971	. . 3 ⊢ ∪x ∈ B C = {y ∣ ∃x ∈ B y ∈ C}
7	5, 6	elab2g 2987	. 2 ⊢ (A ∈ V → (A ∈ ∪x ∈ B C ↔ ∃x ∈ B A ∈ C))
8	1, 3, 7	pm5.21nii 342	1 ⊢ (A ∈ ∪x ∈ B C ↔ ∃x ∈ B A ∈ C)

Syntax hints:   ↔ wb 176   = wceq 1642   ∈ wcel 1710  ∃wrex 2615  Vcvv 2859  ∪ciun 3969

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ral 2619  df-rex 2620  df-v 2861  df-iun 3971

This theorem is referenced by:  iuncom  3975  iuncom4  3976  iunconst  3977  iuniin  3979  iunss1  3980  ss2iun  3984  dfiun2g  3999  ssiun  4008  ssiun2  4009  iunab  4012  iun0  4022  0iun  4023  iunn0  4026  iunin2  4030  iundif2  4033  iindif2  4035  iunxsng  4044  iunun  4046  iunxun  4047  iunxiun  4048  iunpwss  4055  xpiundi  4817  xpiundir  4818  iunxpf  4829  cnvuni  4895  dmuni  4914  rnuni  5038  dfco2  5080  dfco2a  5081  coiun  5090  fun11iun  5305  imaiun  5464  eluniima  5469