Theorem eliun 3972

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

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

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 2802  df-iun 3970

This theorem is referenced by:  iuncom  3974  iuncom4  3975  iunconstm  3976  iuniin  3978  iunss1  3979  ss2iun  3983  dfiun2g  4000  ssiun  4010  ssiun2  4011  iunab  4015  iun0  4025  0iun  4026  iunn0m  4029  iunin2  4032  iundif2ss  4034  iindif2m  4036  iunxsng  4044  iunxsngf  4046  iunun  4047  iunxun  4048  iunxiun  4050  iunpwss  4060  disjiun  4081  triun  4198  iunpw  4575  xpiundi  4782  xpiundir  4783  iunxpf  4876  cnvuni  4914  dmiun  4938  dmuni  4939  rniun  5145  dfco2  5234  dfco2a  5235  coiun  5244  fun11iun  5601  imaiun  5896  eluniimadm  5901  opabex3d  6278  opabex3  6279  smoiun  6462  tfrlemi14d  6494  tfr1onlemres  6510  tfrcllemres  6523  wrdval  11109  fsum2dlemstep  11988  fisumcom2  11992  fsumiun  12031  fprod2dlemstep  12176  fprodcom2fi  12180  ennnfonelemrn  13033  ennnfonelemdm  13034  ctiunctlemf  13052  ctiunctlemfo  13053  imasaddfnlemg  13390  lssats2  14421  clwwlknun  16250