Theorem elex2 2638

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 2160	. . 3 |- ( A e. B -> ( x = A -> x e. B ) )
2	1	alrimiv 1803	. 2 |- ( A e. B -> A. x ( x = A -> x e. B ) )
3		elisset 2636	. 2 |- ( A e. B -> E. x x = A )
4		exim 1536	. 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 1288   = wceq 1290   E.wex 1427   e. wcel 1439

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1382  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-ext 2071

This theorem depends on definitions:  df-bi 116  df-sb 1694  df-clab 2076  df-cleq 2082  df-clel 2085  df-v 2624

This theorem is referenced by:  snmg  3566  oprcl  3654  exmid01  4040  exss  4065  onintrab2im  4350  regexmidlemm  4363  acexmidlem2  5665  frecabcl  6180  ixpm  6503  enm  6592  ssfilem  6647  fin0  6657  fin0or  6658  diffitest  6659  diffisn  6665  infm  6676  inffiexmid  6678  exmidfodomrlemr  6891  exmidfodomrlemrALT  6892  caucvgsrlemasr  7398  gtso  7627  indstr  9144  negm  9163  fzm  9515  fzom  9638  rexfiuz  10485  r19.2uz  10489  resqrexlemgt0  10516  climuni  10744  bezoutlembi  11335  lcmgcdlem  11400  nninfall  12203