Theorem eliun 3916

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

Assertion

Ref	Expression
eliun	⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)

Distinct variable group:   𝑥,𝐴

Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑥)

Proof of Theorem eliun

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 2771	. 2 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 → 𝐴 ∈ V)
2		elex 2771	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	rexlimivw 2607	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4		eleq1 2256	. . . 4 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
5	4	rexbidv 2495	. . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
6		df-iun 3914	. . 3 ⊢ ∪ 𝑥 ∈ 𝐵 𝐶 = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶}
7	5, 6	elab2g 2907	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
8	1, 3, 7	pm5.21nii 705	1 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)

Syntax hints:   ↔ wb 105   = wceq 1364   ∈ wcel 2164  ∃wrex 2473  Vcvv 2760  ∪ ciun 3912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rex 2478  df-v 2762  df-iun 3914

This theorem is referenced by:  iuncom  3918  iuncom4  3919  iunconstm  3920  iuniin  3922  iunss1  3923  ss2iun  3927  dfiun2g  3944  ssiun  3954  ssiun2  3955  iunab  3959  iun0  3969  0iun  3970  iunn0m  3973  iunin2  3976  iundif2ss  3978  iindif2m  3980  iunxsng  3988  iunxsngf  3990  iunun  3991  iunxun  3992  iunxiun  3994  iunpwss  4004  disjiun  4024  triun  4140  iunpw  4511  xpiundi  4717  xpiundir  4718  iunxpf  4810  cnvuni  4848  dmiun  4871  dmuni  4872  rniun  5076  dfco2  5165  dfco2a  5166  coiun  5175  fun11iun  5521  imaiun  5803  eluniimadm  5808  opabex3d  6173  opabex3  6174  smoiun  6354  tfrlemi14d  6386  tfr1onlemres  6402  tfrcllemres  6415  wrdval  10917  fsum2dlemstep  11577  fisumcom2  11581  fsumiun  11620  fprod2dlemstep  11765  fprodcom2fi  11769  ennnfonelemrn  12576  ennnfonelemdm  12577  ctiunctlemf  12595  ctiunctlemfo  12596  imasaddfnlemg  12897  lssats2  13910