Theorem elex2 2697

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 2209	. . 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 2695	. 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 2119

This theorem depends on definitions:  df-bi 116  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-v 2683

This theorem is referenced by:  snmg  3636  oprcl  3724  brm  3973  exmid01  4116  exss  4144  onintrab2im  4429  regexmidlemm  4442  dmxpid  4755  acexmidlem2  5764  frecabcl  6289  ixpm  6617  enm  6707  ssfilem  6762  fin0  6772  fin0or  6773  diffitest  6774  diffisn  6780  infm  6791  inffiexmid  6793  ctssdc  6991  omct  6995  ctssexmid  7017  exmidfodomrlemr  7051  exmidfodomrlemrALT  7052  exmidaclem  7057  caucvgsrlemasr  7591  suplocsrlempr  7608  gtso  7836  sup3exmid  8708  indstr  9381  negm  9400  fzm  9811  fzom  9934  rexfiuz  10754  r19.2uz  10758  resqrexlemgt0  10785  climuni  11055  bezoutlembi  11682  lcmgcdlem  11747  tgioo  12704  nninfall  13193