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  5998  frecabcl  6545  ixpm  6877  en1m  6957  dom1o  6977  dom1oi  6978  enm  6979  ssfilem  7037  fin0  7047  fin0or  7048  diffitest  7049  diffisn  7055  infm  7066  inffiexmid  7068  ctssdc  7280  omct  7284  ctssexmid  7317  exmidfodomrlemr  7380  exmidfodomrlemrALT  7381  acnrcl  7383  exmidaclem  7390  iftrueb01  7408  pw1if  7410  caucvgsrlemasr  7977  suplocsrlempr  7994  gtso  8225  sup3exmid  9104  indstr  9788  negm  9810  fzm  10234  fzom  10361  rexfiuz  11500  r19.2uz  11504  resqrexlemgt0  11531  climuni  11804  bezoutlembi  12526  nninfct  12562  lcmgcdlem  12599  pcprecl  12812  pc2dvds  12853  4sqlem13m  12926  nninfdclemcl  13019  dfgrp3m  13632  issubg2m  13726  issubgrpd2  13727  issubg3  13729  issubg4m  13730  grpissubg  13731  subgintm  13735  nmzsubg  13747  ghmrn  13794  ghmpreima  13803  dvdsr02  14069  01eq0ring  14153  subrgugrp  14204  lmodfopnelem1  14288  rmodislmodlem  14314  rmodislmod  14315  lss1  14326  lsssubg  14341  islss3  14343  islss4  14346  lss1d  14347  lssintclm  14348  dflidl2rng  14445  lidlsubg  14450  cnsubglem  14543  tgioo  15228  elply2  15409  pw1nct  16369  nninfall  16375  nnnninfen  16387