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

Theorem elex2 2629
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 2156 . . 3  |-  ( A  e.  B  ->  (
x  =  A  ->  x  e.  B )
)
21alrimiv 1799 . 2  |-  ( A  e.  B  ->  A. x
( x  =  A  ->  x  e.  B
) )
3 elisset 2627 . 2  |-  ( A  e.  B  ->  E. x  x  =  A )
4 exim 1533 . 2  |-  ( A. x ( x  =  A  ->  x  e.  B )  ->  ( E. x  x  =  A  ->  E. x  x  e.  B ) )
52, 3, 4sylc 61 1  |-  ( A  e.  B  ->  E. x  x  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1285    = wceq 1287   E.wex 1424    e. wcel 1436
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-v 2617
This theorem is referenced by:  snmg  3543  oprcl  3631  exmid01  4008  exss  4030  onintrab2im  4310  regexmidlemm  4323  acexmidlem2  5612  frecabcl  6120  enm  6490  ssfilem  6545  fin0  6555  fin0or  6556  diffitest  6557  diffisn  6563  infm  6574  inffiexmid  6576  exmidfodomrlemr  6775  exmidfodomrlemrALT  6776  caucvgsrlemasr  7282  gtso  7511  indstr  9016  negm  9035  fzm  9387  fzom  9506  rexfiuz  10321  r19.2uz  10325  resqrexlemgt0  10352  climuni  10579  bezoutlembi  10900  lcmgcdlem  10965  nninfall  11369
  Copyright terms: Public domain W3C validator