Theorem elex2 2705

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 2212	. . 3 |- ( A e. B -> ( x = A -> x e. B ) )
2	1	alrimiv 1847	. 2 |- ( A e. B -> A. x ( x = A -> x e. B ) )
3		elisset 2703	. 2 |- ( A e. B -> E. x x = A )
4		exim 1579	. 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 1330   = wceq 1332   E.wex 1469   e. wcel 1481

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 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-v 2691

This theorem is referenced by:  snmg  3649  oprcl  3737  brm  3986  exmid01  4129  exss  4157  onintrab2im  4442  regexmidlemm  4455  dmxpid  4768  acexmidlem2  5779  frecabcl  6304  ixpm  6632  enm  6722  ssfilem  6777  fin0  6787  fin0or  6788  diffitest  6789  diffisn  6795  infm  6806  inffiexmid  6808  ctssdc  7006  omct  7010  ctssexmid  7032  exmidfodomrlemr  7075  exmidfodomrlemrALT  7076  exmidaclem  7081  caucvgsrlemasr  7622  suplocsrlempr  7639  gtso  7867  sup3exmid  8739  indstr  9415  negm  9434  fzm  9849  fzom  9972  rexfiuz  10793  r19.2uz  10797  resqrexlemgt0  10824  climuni  11094  bezoutlembi  11729  lcmgcdlem  11794  tgioo  12754  pw1nct  13371  nninfall  13379