Theorem elex2 2817

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 2815	. 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 2802

This theorem is referenced by:  snmg  3788  oprcl  3884  brm  4137  ss1o0el1  4285  exss  4317  onintrab2im  4614  regexmidlemm  4628  reldmm  4948  dmxpid  4951  acexmidlem2  6010  elmpom  6398  frecabcl  6560  ixpm  6894  en1m  6974  dom1o  6997  dom1oi  6998  enm  6999  ssfilem  7057  fin0  7067  fin0or  7068  diffitest  7069  diffisn  7075  infm  7089  inffiexmid  7091  ctssdc  7303  omct  7307  ctssexmid  7340  exmidfodomrlemr  7403  exmidfodomrlemrALT  7404  acnrcl  7406  exmidaclem  7413  iftrueb01  7431  pw1if  7433  caucvgsrlemasr  8000  suplocsrlempr  8017  gtso  8248  sup3exmid  9127  indstr  9817  negm  9839  fzm  10263  fzom  10390  rexfiuz  11540  r19.2uz  11544  resqrexlemgt0  11571  climuni  11844  bezoutlembi  12566  nninfct  12602  lcmgcdlem  12639  pcprecl  12852  pc2dvds  12893  4sqlem13m  12966  nninfdclemcl  13059  dfgrp3m  13672  issubg2m  13766  issubgrpd2  13767  issubg3  13769  issubg4m  13770  grpissubg  13771  subgintm  13775  nmzsubg  13787  ghmrn  13834  ghmpreima  13843  dvdsr02  14109  01eq0ring  14193  subrgugrp  14244  lmodfopnelem1  14328  rmodislmodlem  14354  rmodislmod  14355  lss1  14366  lsssubg  14381  islss3  14383  islss4  14386  lss1d  14387  lssintclm  14388  dflidl2rng  14485  lidlsubg  14490  cnsubglem  14583  tgioo  15268  elply2  15449  edgval  15901  wlkvtxm  16137  pw1nct  16540  nninfall  16547  nnnninfen  16559