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  4571  xpiundi  4777  xpiundir  4778  iunxpf  4870  cnvuni  4908  dmiun  4932  dmuni  4933  rniun  5139  dfco2  5228  dfco2a  5229  coiun  5238  fun11iun  5595  imaiun  5890  eluniimadm  5895  opabex3d  6272  opabex3  6273  smoiun  6453  tfrlemi14d  6485  tfr1onlemres  6501  tfrcllemres  6514  wrdval  11082  fsum2dlemstep  11953  fisumcom2  11957  fsumiun  11996  fprod2dlemstep  12141  fprodcom2fi  12145  ennnfonelemrn  12998  ennnfonelemdm  12999  ctiunctlemf  13017  ctiunctlemfo  13018  imasaddfnlemg  13355  lssats2  14386