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

Theorem sselda 3097
Description: Membership deduction from subclass relationship. (Contributed by NM, 26-Jun-2014.)
Hypothesis
Ref Expression
sseld.1 (𝜑𝐴𝐵)
Assertion
Ref Expression
sselda ((𝜑𝐶𝐴) → 𝐶𝐵)

Proof of Theorem sselda
StepHypRef Expression
1 sseld.1 . . 3 (𝜑𝐴𝐵)
21sseld 3096 . 2 (𝜑 → (𝐶𝐴𝐶𝐵))
32imp 123 1 ((𝜑𝐶𝐴) → 𝐶𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wcel 1480  wss 3071
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-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-in 3077  df-ss 3084
This theorem is referenced by:  pwntru  4122  elrel  4641  ffvresb  5583  1stdm  6080  tfrlem1  6205  tfrlemiubacc  6227  tfr1onlemubacc  6243  tfrcllemubacc  6256  erinxp  6503  fundmen  6700  supisolem  6895  ordiso2  6920  difinfsn  6985  ctssdc  6998  exmidfodomrlemeldju  7055  exmidfodomrlemreseldju  7056  elprnql  7296  elprnqu  7297  suplocexprlemml  7531  axpre-suploclemres  7716  suprleubex  8719  un0addcl  9017  un0mulcl  9018  suprzclex  9156  supminfex  9399  icoshftf1o  9781  elfzom1elfzo  9987  zpnn0elfzo  9991  seq3fveq  10251  monoord2  10257  seq3coll  10592  rexanre  10999  rexico  11000  summodclem2a  11157  isumss  11167  fisumss  11168  fsum3cvg3  11172  fsumsplit  11183  fsum2dlemstep  11210  fisum0diag2  11223  fsumlessfi  11236  fsumabs  11241  telfsumo  11242  fsumparts  11246  fsumrelem  11247  fsumiun  11253  hashuni  11258  binom1dif  11263  isumsplit  11267  isumrpcl  11270  isumlessdc  11272  mertenslemi1  11311  clim2prod  11315  prodfrecap  11322  prodmodclem2a  11352  ennnfonelemfun  11937  ennnfonelemf1  11938  restid2  12139  tgclb  12244  tgidm  12253  tgrest  12348  txcnp  12450  txdis1cn  12457  psmetres2  12512  blpnfctr  12618  xmetresbl  12619  mopni2  12662  mopni3  12663  rnblopn  12668  xmettx  12689  tgioo  12725  fsumcncntop  12735  climcncf  12750  suplociccreex  12781  suplociccex  12782  dedekindicc  12790  ivthdec  12801  dvfgg  12836  dvcnp2cntop  12842  dvaddxxbr  12844  dvcjbr  12851  pwtrufal  13206
  Copyright terms: Public domain W3C validator