Theorem elex2 2820

Description: If a class contains another class, then it contains some set. (Contributed by Alan Sare, 25-Sep-2011.)

Assertion

Ref	Expression
elex2	⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 ∈ 𝐵)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem elex2

Step	Hyp	Ref	Expression
1		eleq1a 2303	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
2	1	alrimiv 1922	. 2 ⊢ (𝐴 ∈ 𝐵 → ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
3		elisset 2818	. 2 ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 = 𝐴)
4		exim 1648	. 2 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥 𝑥 = 𝐴 → ∃𝑥 𝑥 ∈ 𝐵))
5	2, 3, 4	sylc 62	1 ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 ∈ 𝐵)

Syntax hints:   → wi 4  ∀wal 1396   = wceq 1398  ∃wex 1541   ∈ wcel 2202

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-5 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-v 2805

This theorem is referenced by:  snmg  3794  oprcl  3891  brm  4144  ss1o0el1  4293  exss  4325  onintrab2im  4622  regexmidlemm  4636  reldmm  4956  dmxpid  4959  acexmidlem2  6025  elmpom  6412  frecabcl  6608  ixpm  6942  en1m  7022  dom1o  7045  dom1oi  7046  enm  7047  ssfilem  7105  ssfilemd  7107  fin0  7117  fin0or  7118  diffitest  7119  diffisn  7125  infm  7139  inffiexmid  7141  ctssdc  7355  omct  7359  ctssexmid  7392  exmidfodomrlemr  7456  exmidfodomrlemrALT  7457  acnrcl  7459  exmidaclem  7466  iftrueb01  7484  pw1if  7486  caucvgsrlemasr  8053  suplocsrlempr  8070  gtso  8301  sup3exmid  9180  indstr  9870  negm  9892  fzm  10316  fzom  10443  rexfiuz  11610  r19.2uz  11614  resqrexlemgt0  11641  climuni  11914  bezoutlembi  12637  nninfct  12673  lcmgcdlem  12710  pcprecl  12923  pc2dvds  12964  4sqlem13m  13037  nninfdclemcl  13130  dfgrp3m  13743  issubg2m  13837  issubgrpd2  13838  issubg3  13840  issubg4m  13841  grpissubg  13842  subgintm  13846  nmzsubg  13858  ghmrn  13905  ghmpreima  13914  dvdsr02  14181  01eq0ring  14265  subrgugrp  14316  lmodfopnelem1  14400  rmodislmodlem  14426  rmodislmod  14427  lss1  14438  lsssubg  14453  islss3  14455  islss4  14458  lss1d  14459  lssintclm  14460  dflidl2rng  14557  lidlsubg  14562  cnsubglem  14655  tgioo  15345  elply2  15526  edgval  15981  wlkvtxm  16261  pw1nct  16705  nninfall  16715  nnnninfen  16727