Theorem eliun 3969

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 2811	. 2 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 → 𝐴 ∈ V)
2		elex 2811	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	rexlimivw 2644	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4		eleq1 2292	. . . 4 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
5	4	rexbidv 2531	. . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
6		df-iun 3967	. . 3 ⊢ ∪ 𝑥 ∈ 𝐵 𝐶 = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶}
7	5, 6	elab2g 2950	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
8	1, 3, 7	pm5.21nii 709	1 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)

Syntax hints:   ↔ wb 105   = wceq 1395   ∈ wcel 2200  ∃wrex 2509  Vcvv 2799  ∪ ciun 3965

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2801  df-iun 3967

This theorem is referenced by:  iuncom  3971  iuncom4  3972  iunconstm  3973  iuniin  3975  iunss1  3976  ss2iun  3980  dfiun2g  3997  ssiun  4007  ssiun2  4008  iunab  4012  iun0  4022  0iun  4023  iunn0m  4026  iunin2  4029  iundif2ss  4031  iindif2m  4033  iunxsng  4041  iunxsngf  4043  iunun  4044  iunxun  4045  iunxiun  4047  iunpwss  4057  disjiun  4078  triun  4195  iunpw  4572  xpiundi  4779  xpiundir  4780  iunxpf  4873  cnvuni  4911  dmiun  4935  dmuni  4936  rniun  5142  dfco2  5231  dfco2a  5232  coiun  5241  fun11iun  5598  imaiun  5893  eluniimadm  5898  opabex3d  6275  opabex3  6276  smoiun  6458  tfrlemi14d  6490  tfr1onlemres  6506  tfrcllemres  6519  wrdval  11092  fsum2dlemstep  11966  fisumcom2  11970  fsumiun  12009  fprod2dlemstep  12154  fprodcom2fi  12158  ennnfonelemrn  13011  ennnfonelemdm  13012  ctiunctlemf  13030  ctiunctlemfo  13031  imasaddfnlemg  13368  lssats2  14399