Theorem elex2 2819

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 2817	. 2 ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 = 𝐴)
4		exim 1647	. 2 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥 𝑥 = 𝐴 → ∃𝑥 𝑥 ∈ 𝐵))
5	2, 3, 4	sylc 62	1 ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 ∈ 𝐵)

Syntax hints:   → wi 4  ∀wal 1395   = wceq 1397  ∃wex 1540   ∈ 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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  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 2804

This theorem is referenced by:  snmg  3790  oprcl  3886  brm  4139  ss1o0el1  4287  exss  4319  onintrab2im  4616  regexmidlemm  4630  reldmm  4950  dmxpid  4953  acexmidlem2  6014  elmpom  6402  frecabcl  6564  ixpm  6898  en1m  6978  dom1o  7001  dom1oi  7002  enm  7003  ssfilem  7061  ssfilemd  7063  fin0  7073  fin0or  7074  diffitest  7075  diffisn  7081  infm  7095  inffiexmid  7097  ctssdc  7311  omct  7315  ctssexmid  7348  exmidfodomrlemr  7412  exmidfodomrlemrALT  7413  acnrcl  7415  exmidaclem  7422  iftrueb01  7440  pw1if  7442  caucvgsrlemasr  8009  suplocsrlempr  8026  gtso  8257  sup3exmid  9136  indstr  9826  negm  9848  fzm  10272  fzom  10399  rexfiuz  11549  r19.2uz  11553  resqrexlemgt0  11580  climuni  11853  bezoutlembi  12575  nninfct  12611  lcmgcdlem  12648  pcprecl  12861  pc2dvds  12902  4sqlem13m  12975  nninfdclemcl  13068  dfgrp3m  13681  issubg2m  13775  issubgrpd2  13776  issubg3  13778  issubg4m  13779  grpissubg  13780  subgintm  13784  nmzsubg  13796  ghmrn  13843  ghmpreima  13852  dvdsr02  14118  01eq0ring  14202  subrgugrp  14253  lmodfopnelem1  14337  rmodislmodlem  14363  rmodislmod  14364  lss1  14375  lsssubg  14390  islss3  14392  islss4  14395  lss1d  14396  lssintclm  14397  dflidl2rng  14494  lidlsubg  14499  cnsubglem  14592  tgioo  15277  elply2  15458  edgval  15910  wlkvtxm  16190  pw1nct  16604  nninfall  16611  nnnninfen  16623