Theorem elex2 2768

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 2261	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
2	1	alrimiv 1885	. 2 ⊢ (𝐴 ∈ 𝐵 → ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
3		elisset 2766	. 2 ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 = 𝐴)
4		exim 1610	. 2 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥 𝑥 = 𝐴 → ∃𝑥 𝑥 ∈ 𝐵))
5	2, 3, 4	sylc 62	1 ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 ∈ 𝐵)

Syntax hints:   → wi 4  ∀wal 1362   = wceq 1364  ∃wex 1503   ∈ wcel 2160

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-v 2754

This theorem is referenced by:  snmg  3725  oprcl  3817  brm  4068  ss1o0el1  4215  exss  4245  onintrab2im  4535  regexmidlemm  4549  dmxpid  4866  acexmidlem2  5892  frecabcl  6423  ixpm  6755  enm  6845  ssfilem  6902  fin0  6912  fin0or  6913  diffitest  6914  diffisn  6920  infm  6931  inffiexmid  6933  ctssdc  7141  omct  7145  ctssexmid  7177  exmidfodomrlemr  7230  exmidfodomrlemrALT  7231  exmidaclem  7236  caucvgsrlemasr  7818  suplocsrlempr  7835  gtso  8065  sup3exmid  8943  indstr  9622  negm  9644  fzm  10067  fzom  10193  rexfiuz  11029  r19.2uz  11033  resqrexlemgt0  11060  climuni  11332  bezoutlembi  12037  lcmgcdlem  12108  pcprecl  12320  pc2dvds  12361  4sqlem13m  12434  nninfdclemcl  12498  dfgrp3m  13040  issubg2m  13125  issubgrpd2  13126  issubg3  13128  issubg4m  13129  grpissubg  13130  subgintm  13134  nmzsubg  13146  ghmrn  13193  ghmpreima  13202  dvdsr02  13452  01eq0ring  13533  subrgugrp  13584  lmodfopnelem1  13637  rmodislmodlem  13663  rmodislmod  13664  lss1  13675  lsssubg  13690  islss3  13692  islss4  13695  lss1d  13696  lssintclm  13697  dflidl2rng  13794  lidlsubg  13799  cnsubglem  13879  tgioo  14498  pw1nct  15206  nninfall  15212