Theorem elex2 2816

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 2301	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
2	1	alrimiv 1920	. 2 ⊢ (𝐴 ∈ 𝐵 → ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
3		elisset 2814	. 2 ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 = 𝐴)
4		exim 1645	. 2 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥 𝑥 = 𝐴 → ∃𝑥 𝑥 ∈ 𝐵))
5	2, 3, 4	sylc 62	1 ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 ∈ 𝐵)

Syntax hints:   → wi 4  ∀wal 1393   = wceq 1395  ∃wex 1538   ∈ wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-v 2801

This theorem is referenced by:  snmg  3785  oprcl  3881  brm  4134  ss1o0el1  4281  exss  4313  onintrab2im  4610  regexmidlemm  4624  reldmm  4942  dmxpid  4945  acexmidlem2  6004  frecabcl  6551  ixpm  6885  en1m  6965  dom1o  6985  dom1oi  6986  enm  6987  ssfilem  7045  fin0  7055  fin0or  7056  diffitest  7057  diffisn  7063  infm  7077  inffiexmid  7079  ctssdc  7291  omct  7295  ctssexmid  7328  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  acnrcl  7394  exmidaclem  7401  iftrueb01  7419  pw1if  7421  caucvgsrlemasr  7988  suplocsrlempr  8005  gtso  8236  sup3exmid  9115  indstr  9800  negm  9822  fzm  10246  fzom  10373  rexfiuz  11515  r19.2uz  11519  resqrexlemgt0  11546  climuni  11819  bezoutlembi  12541  nninfct  12577  lcmgcdlem  12614  pcprecl  12827  pc2dvds  12868  4sqlem13m  12941  nninfdclemcl  13034  dfgrp3m  13647  issubg2m  13741  issubgrpd2  13742  issubg3  13744  issubg4m  13745  grpissubg  13746  subgintm  13750  nmzsubg  13762  ghmrn  13809  ghmpreima  13818  dvdsr02  14084  01eq0ring  14168  subrgugrp  14219  lmodfopnelem1  14303  rmodislmodlem  14329  rmodislmod  14330  lss1  14341  lsssubg  14356  islss3  14358  islss4  14361  lss1d  14362  lssintclm  14363  dflidl2rng  14460  lidlsubg  14465  cnsubglem  14558  tgioo  15243  elply2  15424  wlkvtxm  16081  pw1nct  16428  nninfall  16435  nnnninfen  16447