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

Theorem ssel 2994
Description: Membership relationships follow from a subclass relationship. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
ssel  |-  ( A 
C_  B  ->  ( C  e.  A  ->  C  e.  B ) )

Proof of Theorem ssel
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 dfss2 2989 . . . . . 6  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
21biimpi 118 . . . . 5  |-  ( A 
C_  B  ->  A. x
( x  e.  A  ->  x  e.  B ) )
3219.21bi 1491 . . . 4  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
43anim2d 330 . . 3  |-  ( A 
C_  B  ->  (
( x  =  C  /\  x  e.  A
)  ->  ( x  =  C  /\  x  e.  B ) ) )
54eximdv 1802 . 2  |-  ( A 
C_  B  ->  ( E. x ( x  =  C  /\  x  e.  A )  ->  E. x
( x  =  C  /\  x  e.  B
) ) )
6 df-clel 2078 . 2  |-  ( C  e.  A  <->  E. x
( x  =  C  /\  x  e.  A
) )
7 df-clel 2078 . 2  |-  ( C  e.  B  <->  E. x
( x  =  C  /\  x  e.  B
) )
85, 6, 73imtr4g 203 1  |-  ( A 
C_  B  ->  ( C  e.  A  ->  C  e.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102   A.wal 1283    = wceq 1285   E.wex 1422    e. wcel 1434    C_ wss 2974
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 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-11 1438  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-in 2980  df-ss 2987
This theorem is referenced by:  ssel2  2995  sseli  2996  sseld  2999  sstr2  3007  ssralv  3059  ssrexv  3060  ralss  3061  rexss  3062  ssconb  3106  sscon  3107  ssdif  3108  unss1  3142  ssrin  3198  difin2  3233  reuss2  3251  reupick  3255  sssnm  3554  uniss  3630  ss2iun  3701  ssiun  3728  iinss  3737  disjss2  3777  disjss1  3780  pwnss  3941  sspwb  3979  ssopab2b  4039  soss  4077  sucssel  4187  ssorduni  4239  onintonm  4269  onnmin  4319  ssnel  4320  wessep  4328  ssrel  4454  ssrel2  4456  ssrelrel  4466  xpss12  4473  cnvss  4536  dmss  4562  elreldm  4588  dmcosseq  4631  relssres  4676  iss  4684  resopab2  4685  issref  4737  ssrnres  4793  dfco2a  4851  cores  4854  funssres  4972  fununi  4998  funimaexglem  5013  dfimafn  5254  funimass4  5256  funimass3  5315  dff4im  5345  funfvima2  5423  funfvima3  5424  f1elima  5444  riotass2  5525  ssoprab2b  5593  resoprab2  5629  releldm2  5842  reldmtpos  5902  dmtpos  5905  rdgss  6032  negf1o  7553  lbreu  8090  lbinf  8093  eqreznegel  8780  negm  8781  iccsupr  9065  negfi  10248  isumrblem  10337  bdop  10824  bj-nnen2lp  10907
  Copyright terms: Public domain W3C validator