Theorem eliun 3974

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 2814	. 2 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 → 𝐴 ∈ V)
2		elex 2814	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	rexlimivw 2646	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4		eleq1 2294	. . . 4 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
5	4	rexbidv 2533	. . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
6		df-iun 3972	. . 3 ⊢ ∪ 𝑥 ∈ 𝐵 𝐶 = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶}
7	5, 6	elab2g 2953	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
8	1, 3, 7	pm5.21nii 711	1 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)

Syntax hints:   ↔ wb 105   = wceq 1397   ∈ wcel 2202  ∃wrex 2511  Vcvv 2802  ∪ ciun 3970

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-v 2804  df-iun 3972

This theorem is referenced by:  iuncom  3976  iuncom4  3977  iunconstm  3978  iuniin  3980  iunss1  3981  ss2iun  3985  dfiun2g  4002  ssiun  4012  ssiun2  4013  iunab  4017  iun0  4027  0iun  4028  iunn0m  4031  iunin2  4034  iundif2ss  4036  iindif2m  4038  iunxsng  4046  iunxsngf  4048  iunun  4049  iunxun  4050  iunxiun  4052  iunpwss  4062  disjiun  4083  triun  4200  iunpw  4577  xpiundi  4784  xpiundir  4785  iunxpf  4878  cnvuni  4916  dmiun  4940  dmuni  4941  rniun  5147  dfco2  5236  dfco2a  5237  coiun  5246  fun11iun  5604  imaiun  5901  eluniimadm  5906  opabex3d  6283  opabex3  6284  smoiun  6467  tfrlemi14d  6499  tfr1onlemres  6515  tfrcllemres  6528  wrdval  11117  fsum2dlemstep  11997  fisumcom2  12001  fsumiun  12040  fprod2dlemstep  12185  fprodcom2fi  12189  ennnfonelemrn  13042  ennnfonelemdm  13043  ctiunctlemf  13061  ctiunctlemfo  13062  imasaddfnlemg  13399  lssats2  14431  clwwlknun  16295