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

Theorem ssrdv 2979
Description: Deduction rule 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 1770 . 2 (𝜑 → ∀𝑥(𝑥𝐴𝑥𝐵))
3 dfss2 2962 . 2 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
42, 3sylibr 141 1 (𝜑𝐴𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1257  wcel 1409  wss 2945
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-11 1413  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-in 2952  df-ss 2959
This theorem is referenced by:  sscon  3105  ssdif  3106  unss1  3140  ssrin  3190  eq0rdv  3289  uniss  3629  intss1  3658  intmin  3663  intssunim  3665  iunss1  3696  iinss1  3697  ss2iun  3700  ssiun  3727  ssiun2  3728  iinss  3736  iinss2  3737  trintssmOLD  3899  sspwb  3980  tron  4147  ssorduni  4241  ordsson  4246  ordpwsucss  4319  xpsspw  4478  relop  4514  dmss  4562  dmcosseq  4631  ssrnres  4791  chfnrn  5306  ffnfv  5351  f1imass  5441  fo1stresm  5816  fo2ndresm  5817  fo2ndf  5876  reldmtpos  5899  smoiun  5947  tfrlemi14d  5978  nndifsnid  6111  qsss  6196  fidifsnid  6363  onunsnss  6386  addnqprlemrl  6713  addnqprlemru  6714  addnqprlemfl  6715  addnqprlemfu  6716  mulnqprlemrl  6729  mulnqprlemru  6730  mulnqprlemfl  6731  mulnqprlemfu  6732  distrlem1prl  6738  distrlem1pru  6739  distrlem5prl  6742  distrlem5pru  6743  ltprordil  6745  ltexprlemfl  6765  ltexprlemrl  6766  ltexprlemfu  6767  ltexprlemru  6768  addcanprleml  6770  addcanprlemu  6771  recexprlem1ssl  6789  recexprlem1ssu  6790  recexprlemss1l  6791  recexprlemss1u  6792  aptiprleml  6795  aptiprlemu  6796  cauappcvgprlemladdfu  6810  cauappcvgprlemladdfl  6811  cauappcvgprlemladdru  6812  cauappcvgprlemladdrl  6813  caucvgprlemladdfu  6833  caucvgprlemladdrl  6834  peano5uzti  8405  uzss  8589  ixxdisj  8873  ixxss1  8874  ixxss2  8875  ixxss12  8876  iocssre  8923  icossre  8924  iccssre  8925  icodisj  8961  fzss1  9028  fzss2  9029  fzoss1  9129  fzosplit  9135  fzouzsplit  9137  ssfzo12bi  9183  frecuzrdgfn  9362  ovshftex  9648
  Copyright terms: Public domain W3C validator