Theorem eliun 3974

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 2868	. 2 ⊢ (A ∈ ∪x ∈ B C → A ∈ V)
2		elex 2868	. . 3 ⊢ (A ∈ C → A ∈ V)
3	2	rexlimivw 2735	. 2 ⊢ (∃x ∈ B A ∈ C → A ∈ V)
4		eleq1 2413	. . . 4 ⊢ (y = A → (y ∈ C ↔ A ∈ C))
5	4	rexbidv 2636	. . 3 ⊢ (y = A → (∃x ∈ B y ∈ C ↔ ∃x ∈ B A ∈ C))
6		df-iun 3972	. . 3 ⊢ ∪x ∈ B C = {y ∣ ∃x ∈ B y ∈ C}
7	5, 6	elab2g 2988	. 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 2616  Vcvv 2860  ∪ciun 3970

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 2479  df-ral 2620  df-rex 2621  df-v 2862  df-iun 3972

This theorem is referenced by:  iuncom  3976  iuncom4  3977  iunconst  3978  iuniin  3980  iunss1  3981  ss2iun  3985  dfiun2g  4000  ssiun  4009  ssiun2  4010  iunab  4013  iun0  4023  0iun  4024  iunn0  4027  iunin2  4031  iundif2  4034  iindif2  4036  iunxsng  4045  iunun  4047  iunxun  4048  iunxiun  4049  iunpwss  4056  xpiundi  4818  xpiundir  4819  iunxpf  4830  cnvuni  4896  dmuni  4915  rnuni  5039  dfco2  5081  dfco2a  5082  coiun  5091  fun11iun  5306  imaiun  5465  eluniima  5470