Theorem eliun 3855

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 2723	. 2 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 → 𝐴 ∈ V)
2		elex 2723	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	rexlimivw 2570	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4		eleq1 2220	. . . 4 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
5	4	rexbidv 2458	. . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
6		df-iun 3853	. . 3 ⊢ ∪ 𝑥 ∈ 𝐵 𝐶 = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶}
7	5, 6	elab2g 2859	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
8	1, 3, 7	pm5.21nii 694	1 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)

Syntax hints:   ↔ wb 104   = wceq 1335   ∈ wcel 2128  ∃wrex 2436  Vcvv 2712  ∪ ciun 3851

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ral 2440  df-rex 2441  df-v 2714  df-iun 3853

This theorem is referenced by:  iuncom  3857  iuncom4  3858  iunconstm  3859  iuniin  3861  iunss1  3862  ss2iun  3866  dfiun2g  3883  ssiun  3893  ssiun2  3894  iunab  3897  iun0  3907  0iun  3908  iunn0m  3911  iunin2  3914  iundif2ss  3916  iindif2m  3918  iunxsng  3926  iunxsngf  3928  iunun  3929  iunxun  3930  iunxiun  3932  iunpwss  3942  disjiun  3962  triun  4077  iunpw  4442  xpiundi  4646  xpiundir  4647  iunxpf  4736  cnvuni  4774  dmiun  4797  dmuni  4798  rniun  4998  dfco2  5087  dfco2a  5088  coiun  5097  fun11iun  5437  imaiun  5712  eluniimadm  5717  opabex3d  6071  opabex3  6072  smoiun  6250  tfrlemi14d  6282  tfr1onlemres  6298  tfrcllemres  6311  fsum2dlemstep  11342  fisumcom2  11346  fsumiun  11385  fprod2dlemstep  11530  fprodcom2fi  11534  ennnfonelemrn  12218  ennnfonelemdm  12219  ctiunctlemf  12237  ctiunctlemfo  12238