Theorem eliun 3892

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

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

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 2741  df-iun 3890

This theorem is referenced by:  iuncom  3894  iuncom4  3895  iunconstm  3896  iuniin  3898  iunss1  3899  ss2iun  3903  dfiun2g  3920  ssiun  3930  ssiun2  3931  iunab  3935  iun0  3945  0iun  3946  iunn0m  3949  iunin2  3952  iundif2ss  3954  iindif2m  3956  iunxsng  3964  iunxsngf  3966  iunun  3967  iunxun  3968  iunxiun  3970  iunpwss  3980  disjiun  4000  triun  4116  iunpw  4482  xpiundi  4686  xpiundir  4687  iunxpf  4777  cnvuni  4815  dmiun  4838  dmuni  4839  rniun  5041  dfco2  5130  dfco2a  5131  coiun  5140  fun11iun  5484  imaiun  5764  eluniimadm  5769  opabex3d  6125  opabex3  6126  smoiun  6305  tfrlemi14d  6337  tfr1onlemres  6353  tfrcllemres  6366  fsum2dlemstep  11445  fisumcom2  11449  fsumiun  11488  fprod2dlemstep  11633  fprodcom2fi  11637  ennnfonelemrn  12423  ennnfonelemdm  12424  ctiunctlemf  12442  ctiunctlemfo  12443  imasaddfnlemg  12741  lssats2  13539