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

Theorem ssrdv 3103
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 1846 . 2 (𝜑 → ∀𝑥(𝑥𝐴𝑥𝐵))
3 dfss2 3086 . 2 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
42, 3sylibr 133 1 (𝜑𝐴𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1329  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:  eqelssd  3116  sscon  3210  ssdif  3211  unss1  3245  ssrin  3301  eq0rdv  3407  uniss  3757  intss1  3786  intmin  3791  intssunim  3793  iunss1  3824  iinss1  3825  ss2iun  3828  ssiun  3855  ssiun2  3856  iinss  3864  iinss2  3865  exmidundif  4129  exmidundifim  4130  sspwb  4138  tron  4304  ssorduni  4403  ordsson  4408  ordpwsucss  4482  xpsspw  4651  relop  4689  dmss  4738  dmcosseq  4810  ssrnres  4981  chfnrn  5531  ffnfv  5578  f1imass  5675  fo1stresm  6059  fo2ndresm  6060  oprssdmm  6069  fo2ndf  6124  reldmtpos  6150  smoiun  6198  tfrlemi14d  6230  tfr1onlemres  6246  tfri1dALT  6248  tfrcllemres  6259  dcdifsnid  6400  qsss  6488  pmss12g  6569  mapss  6585  ixpssmap2g  6621  ixpssmapg  6622  en2eqpr  6801  exmidpw  6802  onunsnss  6805  undifdcss  6811  ssfii  6862  fiss  6865  difinfsn  6985  addnqprlemrl  7372  addnqprlemru  7373  addnqprlemfl  7374  addnqprlemfu  7375  mulnqprlemrl  7388  mulnqprlemru  7389  mulnqprlemfl  7390  mulnqprlemfu  7391  distrlem1prl  7397  distrlem1pru  7398  distrlem5prl  7401  distrlem5pru  7402  ltprordil  7404  ltexprlemfl  7424  ltexprlemrl  7425  ltexprlemfu  7426  ltexprlemru  7427  addcanprleml  7429  addcanprlemu  7430  recexprlem1ssl  7448  recexprlem1ssu  7449  recexprlemss1l  7450  recexprlemss1u  7451  aptiprleml  7454  aptiprlemu  7455  cauappcvgprlemladdfu  7469  cauappcvgprlemladdfl  7470  cauappcvgprlemladdru  7471  cauappcvgprlemladdrl  7472  caucvgprlemladdfu  7492  caucvgprlemladdrl  7493  suplocexprlemss  7530  suplocexprlemex  7537  peano5uzti  9166  uzss  9353  ixxdisj  9693  ixxss1  9694  ixxss2  9695  ixxss12  9696  iocssre  9743  icossre  9744  iccssre  9745  icodisj  9782  fzss1  9850  fzss2  9851  fzoss1  9955  fzosplit  9961  fzouzsplit  9963  ssfzo12bi  10009  frecuzrdgtcl  10192  frecuzrdgdomlem  10197  ovshftex  10598  summodclem2a  11157  fsum3cvg3  11172  fsum2dlemstep  11210  prodmodclem2a  11352  phimullem  11908  ennnfonelemdm  11940  bastg  12240  tgss  12242  tgtop  12247  tgidm  12253  neisspw  12327  topssnei  12341  tgrest  12348  ssrest  12361  cnss1  12405  cnss2  12406  cnsscnp  12408  cnrest2r  12416  txdis  12456  xblss2ps  12583  xblss2  12584  xmettxlem  12688  xmettx  12689  cncfss  12749  cnopnap  12773  dvfgg  12836  dvcj  12852
  Copyright terms: Public domain W3C validator