Theorem elex2 2702

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 2211	. . 3 |- ( A e. B -> ( x = A -> x e. B ) )
2	1	alrimiv 1846	. 2 |- ( A e. B -> A. x ( x = A -> x e. B ) )
3		elisset 2700	. 2 |- ( A e. B -> E. x x = A )
4		exim 1578	. 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 1329   = wceq 1331   E.wex 1468   e. wcel 1480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-v 2688

This theorem is referenced by:  snmg  3641  oprcl  3729  brm  3978  exmid01  4121  exss  4149  onintrab2im  4434  regexmidlemm  4447  dmxpid  4760  acexmidlem2  5771  frecabcl  6296  ixpm  6624  enm  6714  ssfilem  6769  fin0  6779  fin0or  6780  diffitest  6781  diffisn  6787  infm  6798  inffiexmid  6800  ctssdc  6998  omct  7002  ctssexmid  7024  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  exmidaclem  7064  caucvgsrlemasr  7598  suplocsrlempr  7615  gtso  7843  sup3exmid  8715  indstr  9388  negm  9407  fzm  9818  fzom  9941  rexfiuz  10761  r19.2uz  10765  resqrexlemgt0  10792  climuni  11062  bezoutlembi  11693  lcmgcdlem  11758  tgioo  12715  nninfall  13204