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  6675  mapm  6975  ixpm  7018  en1m  7098  dom1o  7122  dom1oi  7123  enm  7124  ssfilem  7183  ssfilemd  7185  fin0  7195  fin0or  7196  diffitest  7197  diffisn  7203  infm  7217  inffiexmid  7219  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  10008  negm  10030  fzm  10458  fzom  10588  rexfiuz  11776  r19.2uz  11780  resqrexlemgt0  11807  climuni  12083  bezoutlembi  12806  nninfct  12842  lcmgcdlem  12879  pcprecl  13096  pc2dvds  13137  4sqlem13m  13210  nninfdclemcl  13396  dfgrp3m  13962  issubg2m  14050  issubgrpd2  14051  issubg3  14053  issubg4m  14054  grpissubg  14055  subgintm  14059  nmzsubg  14071  ghmrn  14118  ghmpreima  14127  dvdsr02  14520  01eq0ring  14604  subrgugrp  14656  lmodfopnelem1  14769  rmodislmodlem  14795  rmodislmod  14796  lss1  14807  lsssubg  14822  islss3  14824  islss4  14827  lss1d  14828  lssintclm  14829  dflidl2rng  14926  lidlsubg  14931  cnsubglem  15024  asplss  15124  aspsubrg  15126  tgioo  15797  elply2  15978  edgval  16523  wlkvtxm  16803  pw1nct  17255  rabid1o  17256  stnot  17261  nninfall  17275  nnnninfen  17287