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	|- ( A e. B -> E. x x e. B )

Distinct variable groups:   x, A   x, B

Proof of Theorem elex2

Step	Hyp	Ref	Expression
1		eleq1a 2301	. . 3 |- ( A e. B -> ( x = A -> x e. B ) )
2	1	alrimiv 1920	. 2 |- ( A e. B -> A. x ( x = A -> x e. B ) )
3		elisset 2814	. 2 |- ( A e. B -> E. x x = A )
4		exim 1645	. 2 |- ( A. x ( x = A -> x e. B ) -> ( E. x x = A -> E. x x e. B ) )
5	2, 3, 4	sylc 62	1 |- ( A e. B -> E. x x e. B )

Syntax hints:   -> wi 4   A.wal 1393   = wceq 1395   E.wex 1538   e. 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  3785  oprcl  3881  brm  4134  ss1o0el1  4281  exss  4313  onintrab2im  4610  regexmidlemm  4624  reldmm  4942  dmxpid  4945  acexmidlem2  6004  frecabcl  6551  ixpm  6885  en1m  6965  dom1o  6985  dom1oi  6986  enm  6987  ssfilem  7045  fin0  7055  fin0or  7056  diffitest  7057  diffisn  7063  infm  7077  inffiexmid  7079  ctssdc  7291  omct  7295  ctssexmid  7328  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  acnrcl  7394  exmidaclem  7401  iftrueb01  7419  pw1if  7421  caucvgsrlemasr  7988  suplocsrlempr  8005  gtso  8236  sup3exmid  9115  indstr  9800  negm  9822  fzm  10246  fzom  10373  rexfiuz  11516  r19.2uz  11520  resqrexlemgt0  11547  climuni  11820  bezoutlembi  12542  nninfct  12578  lcmgcdlem  12615  pcprecl  12828  pc2dvds  12869  4sqlem13m  12942  nninfdclemcl  13035  dfgrp3m  13648  issubg2m  13742  issubgrpd2  13743  issubg3  13745  issubg4m  13746  grpissubg  13747  subgintm  13751  nmzsubg  13763  ghmrn  13810  ghmpreima  13819  dvdsr02  14085  01eq0ring  14169  subrgugrp  14220  lmodfopnelem1  14304  rmodislmodlem  14330  rmodislmod  14331  lss1  14342  lsssubg  14357  islss3  14359  islss4  14362  lss1d  14363  lssintclm  14364  dflidl2rng  14461  lidlsubg  14466  cnsubglem  14559  tgioo  15244  elply2  15425  wlkvtxm  16086  pw1nct  16456  nninfall  16463  nnnninfen  16475