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

Theorem ssrdv 3144
Description: Deduction based on subclass definition. (Contributed by NM, 15-Nov-1995.)
Hypothesis
Ref Expression
ssrdv.1 (𝜑 → (𝑥𝐴𝑥𝐵))
Assertion
Ref Expression
ssrdv (𝜑𝐴𝐵)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜑,𝑥

Proof of Theorem ssrdv
StepHypRef Expression
1 ssrdv.1 . . 3 (𝜑 → (𝑥𝐴𝑥𝐵))
21alrimiv 1861 . 2 (𝜑 → ∀𝑥(𝑥𝐴𝑥𝐵))
3 dfss2 3127 . 2 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
42, 3sylibr 133 1 (𝜑𝐴𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1340  wcel 2135  wss 3112
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 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-11 1493  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146
This theorem depends on definitions:  df-bi 116  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-in 3118  df-ss 3125
This theorem is referenced by:  eqelssd  3157  sscon  3252  ssdif  3253  unss1  3287  ssrin  3343  eq0rdv  3449  uniss  3805  intss1  3834  intmin  3839  intssunim  3841  iunss1  3872  iinss1  3873  ss2iun  3876  ssiun  3903  ssiun2  3904  iinss  3912  iinss2  3913  exmidundif  4180  exmidundifim  4181  sspwb  4189  tron  4355  ssorduni  4459  ordsson  4464  ordpwsucss  4539  xpsspw  4711  relop  4749  dmss  4798  dmcosseq  4870  ssrnres  5041  chfnrn  5591  ffnfv  5638  f1imass  5737  fo1stresm  6122  fo2ndresm  6123  oprssdmm  6132  fo2ndf  6187  reldmtpos  6213  smoiun  6261  tfrlemi14d  6293  tfr1onlemres  6309  tfri1dALT  6311  tfrcllemres  6322  dcdifsnid  6464  qsss  6552  pmss12g  6633  mapss  6649  ixpssmap2g  6685  ixpssmapg  6686  en2eqpr  6865  exmidpw  6866  exmidpweq  6867  onunsnss  6874  undifdcss  6880  ssfii  6931  fiss  6934  difinfsn  7057  addnqprlemrl  7490  addnqprlemru  7491  addnqprlemfl  7492  addnqprlemfu  7493  mulnqprlemrl  7506  mulnqprlemru  7507  mulnqprlemfl  7508  mulnqprlemfu  7509  distrlem1prl  7515  distrlem1pru  7516  distrlem5prl  7519  distrlem5pru  7520  ltprordil  7522  ltexprlemfl  7542  ltexprlemrl  7543  ltexprlemfu  7544  ltexprlemru  7545  addcanprleml  7547  addcanprlemu  7548  recexprlem1ssl  7566  recexprlem1ssu  7567  recexprlemss1l  7568  recexprlemss1u  7569  aptiprleml  7572  aptiprlemu  7573  cauappcvgprlemladdfu  7587  cauappcvgprlemladdfl  7588  cauappcvgprlemladdru  7589  cauappcvgprlemladdrl  7590  caucvgprlemladdfu  7610  caucvgprlemladdrl  7611  suplocexprlemss  7648  suplocexprlemex  7655  peano5uzti  9291  uzss  9478  ixxdisj  9831  ixxss1  9832  ixxss2  9833  ixxss12  9834  iocssre  9881  icossre  9882  iccssre  9883  icodisj  9920  fzss1  9989  fzss2  9990  fzoss1  10097  fzosplit  10103  fzouzsplit  10105  ssfzo12bi  10151  frecuzrdgtcl  10338  frecuzrdgdomlem  10343  ovshftex  10751  summodclem2a  11312  fsum3cvg3  11327  fsum2dlemstep  11365  prodmodclem2a  11507  fprod2dlemstep  11553  phimullem  12146  1arith  12286  ennnfonelemdm  12316  bastg  12628  tgss  12630  tgtop  12635  tgidm  12641  neisspw  12715  topssnei  12729  tgrest  12736  ssrest  12749  cnss1  12793  cnss2  12794  cnsscnp  12796  cnrest2r  12804  txdis  12844  xblss2ps  12971  xblss2  12972  xmettxlem  13076  xmettx  13077  cncfss  13137  cnopnap  13161  dvfgg  13224  dvcj  13240
  Copyright terms: Public domain W3C validator