Theorem eliun 3975

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 2813	. 2 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 → 𝐴 ∈ V)
2		elex 2813	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	rexlimivw 2645	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4		eleq1 2293	. . . 4 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
5	4	rexbidv 2532	. . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
6		df-iun 3973	. . 3 ⊢ ∪ 𝑥 ∈ 𝐵 𝐶 = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶}
7	5, 6	elab2g 2952	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
8	1, 3, 7	pm5.21nii 711	1 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)

Syntax hints:   ↔ wb 105   = wceq 1397   ∈ wcel 2201  ∃wrex 2510  Vcvv 2801  ∪ ciun 3971

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 2212

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-ral 2514  df-rex 2515  df-v 2803  df-iun 3973

This theorem is referenced by:  iuncom  3977  iuncom4  3978  iunconstm  3979  iuniin  3981  iunss1  3982  ss2iun  3986  dfiun2g  4003  ssiun  4013  ssiun2  4014  iunab  4018  iun0  4028  0iun  4029  iunn0m  4032  iunin2  4035  iundif2ss  4037  iindif2m  4039  iunxsng  4047  iunxsngf  4049  iunun  4050  iunxun  4051  iunxiun  4053  iunpwss  4063  disjiun  4084  triun  4201  iunpw  4579  xpiundi  4786  xpiundir  4787  iunxpf  4880  cnvuni  4918  dmiun  4942  dmuni  4943  rniun  5149  dfco2  5238  dfco2a  5239  coiun  5248  fun11iun  5607  imaiun  5906  eluniimadm  5911  opabex3d  6288  opabex3  6289  smoiun  6472  tfrlemi14d  6504  tfr1onlemres  6520  tfrcllemres  6533  wrdval  11125  fsum2dlemstep  12018  fisumcom2  12022  fsumiun  12061  fprod2dlemstep  12206  fprodcom2fi  12210  ennnfonelemrn  13063  ennnfonelemdm  13064  ctiunctlemf  13082  ctiunctlemfo  13083  imasaddfnlemg  13420  lssats2  14452  clwwlknun  16321