Theorem elex2 2838

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 2310	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
2	1	alrimiv 1927	. 2 ⊢ (𝐴 ∈ 𝐵 → ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
3		elisset 2836	. 2 ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 = 𝐴)
4		exim 1652	. 2 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥 𝑥 = 𝐴 → ∃𝑥 𝑥 ∈ 𝐵))
5	2, 3, 4	sylc 62	1 ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 ∈ 𝐵)

This proof depends on syntax axioms:   → wi 4  ∀wal 1400   = wceq 1402  ∃wex 1545   ∈ wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-v 2823

This theorem is used by:  snmg  3831  oprcl  3928  brm  4182  ss1o0el1  4336  exss  4369  onintrab2im  4667  regexmidlemm  4681  reldmm  5002  dmxpid  5005  mptmex  5948  acexmidlem2  6085  elmpom  6478  frecabcl  6674  ixpm  7016  en1m  7096  dom1o  7120  dom1oi  7121  enm  7122  ssfilem  7181  ssfilemd  7183  fin0  7193  fin0or  7194  diffitest  7195  diffisn  7201  infm  7215  inffiexmid  7217  ctssdc  7459  omct  7463  ctssexmid  7496  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  acnrcl  7563  exmidaclem  7570  iftrueb01  7588  pw1if  7590  caucvgsrlemasr  8163  suplocsrlempr  8180  gtso  8410  sup3exmid  9295  indstr  10009  negm  10031  fzm  10459  fzom  10589  rexfiuz  11777  r19.2uz  11781  resqrexlemgt0  11808  climuni  12084  bezoutlembi  12807  nninfct  12843  lcmgcdlem  12880  pcprecl  13097  pc2dvds  13138  4sqlem13m  13211  nninfdclemcl  13397  dfgrp3m  13963  issubg2m  14051  issubgrpd2  14052  issubg3  14054  issubg4m  14055  grpissubg  14056  subgintm  14060  nmzsubg  14072  ghmrn  14119  ghmpreima  14128  dvdsr02  14521  01eq0ring  14605  subrgugrp  14657  lmodfopnelem1  14770  rmodislmodlem  14796  rmodislmod  14797  lss1  14808  lsssubg  14823  islss3  14825  islss4  14828  lss1d  14829  lssintclm  14830  dflidl2rng  14927  lidlsubg  14932  cnsubglem  15025  asplss  15125  aspsubrg  15127  tgioo  15780  elply2  15961  edgval  16506  wlkvtxm  16786  pw1nct  17238  rabid1o  17239  stnot  17244  nninfall  17258  nnnninfen  17270