ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  elex2 Unicode version

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
StepHypRef Expression
1 eleq1a 2211 . . 3  |-  ( A  e.  B  ->  (
x  =  A  ->  x  e.  B )
)
21alrimiv 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 ) )
52, 3, 4sylc 62 1  |-  ( A  e.  B  ->  E. x  x  e.  B )
Colors of variables: wff set class
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  7605  suplocsrlempr  7622  gtso  7850  sup3exmid  8722  indstr  9395  negm  9414  fzm  9825  fzom  9948  rexfiuz  10768  r19.2uz  10772  resqrexlemgt0  10799  climuni  11069  bezoutlembi  11700  lcmgcdlem  11765  tgioo  12725  nninfall  13218
  Copyright terms: Public domain W3C validator