Theorem eliun 1998

Description: Membership in indexed union.

Assertion

Ref	Expression
eliun	⊢ (A ∈ ∪x ∈ B C ↔ ∃x ∈ B A ∈ C)

Distinct variable group(s):   x,A

Proof of Theorem eliun

Step	Hyp	Ref	Expression
1		elisset 1354	. 2 ⊢ (A ∈ ∪x ∈ B C → A ∈ V)
2		elisset 1354	. . . 4 ⊢ (A ∈ C → A ∈ V)
3	2	a1i 7	. . 3 ⊢ (x ∈ B → (A ∈ C → A ∈ V))
4	3	r19.23aiv 1284	. 2 ⊢ (∃x ∈ B A ∈ C → A ∈ V)
5		eleq1 1149	. . . 4 ⊢ (y = A → (y ∈ C ↔ A ∈ C))
6	5	birexdv 1220	. . 3 ⊢ (y = A → (∃x ∈ B y ∈ C ↔ ∃x ∈ B A ∈ C))
7		df-iun 1996	. . 3 ⊢ ∪x ∈ B C = {y∣∃x ∈ B y ∈ C}
8	6, 7	elab2g 1418	. 2 ⊢ (A ∈ V → (A ∈ ∪x ∈ B C ↔ ∃x ∈ B A ∈ C))
9	1, 4, 8	pm5.21nii 504	1 ⊢ (A ∈ ∪x ∈ B C ↔ ∃x ∈ B A ∈ C)

Syntax hints:   → wi 2   ↔ wb 127   = wceq 1091   ∈ wcel 1092  ∃wrex 1202  Vcvv 1348  ∪ciun 1994

This theorem is referenced by:  iunconst 2000  iuniin 2001  ss2iun 2005  iunss 2017  ssiun 2018  ssiun2 2019  iunrab 2022  iun0 2028  iunn0 2029  iunin2 2030  iundif2 2032  iindif2 2033  iunxsn 2034  iunxun 2035  iununi 2037  iunpwss 2039  iunpw 2040  cnvuni 2521  dmuni 2538  rnuni 2646  imaiun 2650  oalimcl 3162  oaass 3163  trcl 3489  r1tr 3498  r1ord 3499  jech9.3 3510  rankr1 3518  r1pwcl 3530  cardaleph 3690  infxpidmlem6 4938  infxpidmlem7 4939

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-rex 1206  df-v 1349  df-iun 1996

metamath.org