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

Theorem sselda 3067
Description: Membership deduction from subclass relationship. (Contributed by NM, 26-Jun-2014.)
Hypothesis
Ref Expression
sseld.1  |-  ( ph  ->  A  C_  B )
Assertion
Ref Expression
sselda  |-  ( (
ph  /\  C  e.  A )  ->  C  e.  B )

Proof of Theorem sselda
StepHypRef Expression
1 sseld.1 . . 3  |-  ( ph  ->  A  C_  B )
21sseld 3066 . 2  |-  ( ph  ->  ( C  e.  A  ->  C  e.  B ) )
32imp 123 1  |-  ( (
ph  /\  C  e.  A )  ->  C  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    e. wcel 1465    C_ wss 3041
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 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-11 1469  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-in 3047  df-ss 3054
This theorem is referenced by:  pwntru  4092  elrel  4611  ffvresb  5551  1stdm  6048  tfrlem1  6173  tfrlemiubacc  6195  tfr1onlemubacc  6211  tfrcllemubacc  6224  erinxp  6471  fundmen  6668  supisolem  6863  ordiso2  6888  difinfsn  6953  ctssdc  6966  exmidfodomrlemeldju  7023  exmidfodomrlemreseldju  7024  elprnql  7257  elprnqu  7258  suplocexprlemml  7492  axpre-suploclemres  7677  suprleubex  8676  un0addcl  8968  un0mulcl  8969  suprzclex  9107  supminfex  9348  icoshftf1o  9729  elfzom1elfzo  9935  zpnn0elfzo  9939  seq3fveq  10199  monoord2  10205  seq3coll  10540  rexanre  10947  rexico  10948  summodclem2a  11105  isumss  11115  fisumss  11116  fsum3cvg3  11120  fsumsplit  11131  fsum2dlemstep  11158  fisum0diag2  11171  fsumlessfi  11184  fsumabs  11189  telfsumo  11190  fsumparts  11194  fsumrelem  11195  fsumiun  11201  hashuni  11206  binom1dif  11211  isumsplit  11215  isumrpcl  11218  isumlessdc  11220  mertenslemi1  11259  ennnfonelemfun  11841  ennnfonelemf1  11842  restid2  12040  tgclb  12145  tgidm  12154  tgrest  12249  txcnp  12351  txdis1cn  12358  psmetres2  12413  blpnfctr  12519  xmetresbl  12520  mopni2  12563  mopni3  12564  rnblopn  12569  xmettx  12590  tgioo  12626  fsumcncntop  12636  climcncf  12651  suplociccreex  12682  suplociccex  12683  dedekindicc  12691  ivthdec  12702  dvfgg  12737  dvcnp2cntop  12743  dvaddxxbr  12745  dvcjbr  12752  pwtrufal  13088
  Copyright terms: Public domain W3C validator