Theorem elex2 2830

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 2304	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
2	1	alrimiv 1923	. 2 ⊢ (𝐴 ∈ 𝐵 → ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
3		elisset 2828	. 2 ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 = 𝐴)
4		exim 1648	. 2 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥 𝑥 = 𝐴 → ∃𝑥 𝑥 ∈ 𝐵))
5	2, 3, 4	sylc 62	1 ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 ∈ 𝐵)

Syntax hints:   → wi 4  ∀wal 1396   = wceq 1398  ∃wex 1541   ∈ wcel 2203

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-v 2815

This theorem is referenced by:  snmg  3810  oprcl  3907  brm  4160  ss1o0el1  4310  exss  4343  onintrab2im  4640  regexmidlemm  4654  reldmm  4975  dmxpid  4978  acexmidlem2  6047  elmpom  6434  frecabcl  6630  ixpm  6965  en1m  7045  dom1o  7069  dom1oi  7070  enm  7071  ssfilem  7130  ssfilemd  7132  fin0  7142  fin0or  7143  diffitest  7144  diffisn  7150  infm  7164  inffiexmid  7166  ctssdc  7404  omct  7408  ctssexmid  7441  exmidfodomrlemr  7505  exmidfodomrlemrALT  7506  acnrcl  7508  exmidaclem  7515  iftrueb01  7533  pw1if  7535  caucvgsrlemasr  8105  suplocsrlempr  8122  gtso  8352  sup3exmid  9231  indstr  9925  negm  9947  fzm  10372  fzom  10499  rexfiuz  11674  r19.2uz  11678  resqrexlemgt0  11705  climuni  11978  bezoutlembi  12701  nninfct  12737  lcmgcdlem  12774  pcprecl  12987  pc2dvds  13028  4sqlem13m  13101  nninfdclemcl  13199  dfgrp3m  13812  issubg2m  13906  issubgrpd2  13907  issubg3  13909  issubg4m  13910  grpissubg  13911  subgintm  13915  nmzsubg  13927  ghmrn  13974  ghmpreima  13983  dvdsr02  14250  01eq0ring  14334  subrgugrp  14385  lmodfopnelem1  14472  rmodislmodlem  14498  rmodislmod  14499  lss1  14510  lsssubg  14525  islss3  14527  islss4  14530  lss1d  14531  lssintclm  14532  dflidl2rng  14629  lidlsubg  14634  cnsubglem  14727  tgioo  15419  elply2  15600  edgval  16055  wlkvtxm  16335  pw1nct  16777  nninfall  16787  nnnninfen  16799