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  3784  oprcl  3880  brm  4133  ss1o0el1  4280  exss  4312  onintrab2im  4609  regexmidlemm  4623  reldmm  4941  dmxpid  4944  acexmidlem2  5997  frecabcl  6543  ixpm  6875  en1m  6955  enm  6975  ssfilem  7033  fin0  7043  fin0or  7044  diffitest  7045  diffisn  7051  infm  7062  inffiexmid  7064  ctssdc  7276  omct  7280  ctssexmid  7313  exmidfodomrlemr  7376  exmidfodomrlemrALT  7377  acnrcl  7379  exmidaclem  7386  iftrueb01  7404  pw1if  7406  caucvgsrlemasr  7973  suplocsrlempr  7990  gtso  8221  sup3exmid  9100  indstr  9784  negm  9806  fzm  10230  fzom  10357  rexfiuz  11495  r19.2uz  11499  resqrexlemgt0  11526  climuni  11799  bezoutlembi  12521  nninfct  12557  lcmgcdlem  12594  pcprecl  12807  pc2dvds  12848  4sqlem13m  12921  nninfdclemcl  13014  dfgrp3m  13627  issubg2m  13721  issubgrpd2  13722  issubg3  13724  issubg4m  13725  grpissubg  13726  subgintm  13730  nmzsubg  13742  ghmrn  13789  ghmpreima  13798  dvdsr02  14063  01eq0ring  14147  subrgugrp  14198  lmodfopnelem1  14282  rmodislmodlem  14308  rmodislmod  14309  lss1  14320  lsssubg  14335  islss3  14337  islss4  14340  lss1d  14341  lssintclm  14342  dflidl2rng  14439  lidlsubg  14444  cnsubglem  14537  tgioo  15222  elply2  15403  dom1o  16314  pw1nct  16328  nninfall  16334  nnnninfen  16346