Theorem eliun 3891

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 2749	. 2 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 → 𝐴 ∈ V)
2		elex 2749	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	rexlimivw 2590	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4		eleq1 2240	. . . 4 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
5	4	rexbidv 2478	. . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
6		df-iun 3889	. . 3 ⊢ ∪ 𝑥 ∈ 𝐵 𝐶 = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶}
7	5, 6	elab2g 2885	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
8	1, 3, 7	pm5.21nii 704	1 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)

Syntax hints:   ↔ wb 105   = wceq 1353   ∈ wcel 2148  ∃wrex 2456  Vcvv 2738  ∪ ciun 3887

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2740  df-iun 3889

This theorem is referenced by:  iuncom  3893  iuncom4  3894  iunconstm  3895  iuniin  3897  iunss1  3898  ss2iun  3902  dfiun2g  3919  ssiun  3929  ssiun2  3930  iunab  3934  iun0  3944  0iun  3945  iunn0m  3948  iunin2  3951  iundif2ss  3953  iindif2m  3955  iunxsng  3963  iunxsngf  3965  iunun  3966  iunxun  3967  iunxiun  3969  iunpwss  3979  disjiun  3999  triun  4115  iunpw  4481  xpiundi  4685  xpiundir  4686  iunxpf  4776  cnvuni  4814  dmiun  4837  dmuni  4838  rniun  5040  dfco2  5129  dfco2a  5130  coiun  5139  fun11iun  5483  imaiun  5761  eluniimadm  5766  opabex3d  6122  opabex3  6123  smoiun  6302  tfrlemi14d  6334  tfr1onlemres  6350  tfrcllemres  6363  fsum2dlemstep  11442  fisumcom2  11446  fsumiun  11485  fprod2dlemstep  11630  fprodcom2fi  11634  ennnfonelemrn  12420  ennnfonelemdm  12421  ctiunctlemf  12439  ctiunctlemfo  12440  imasaddfnlemg  12735