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

Theorem ssrdv 2924
Description: Deduction rule based on subclass definition. (Contributed by NM, 15-Nov-1995.)
Hypothesis
Ref Expression
ssrdv.1 (φ → (x Ax B))
Assertion
Ref Expression
ssrdv (φAB)
Distinct variable groups:   x,A   x,B   φ,x

Proof of Theorem ssrdv
StepHypRef Expression
1 ssrdv.1 . . 3 (φ → (x Ax B))
21alrimiv 1732 . 2 (φx(x Ax B))
3 dfss2 2907 . 2 (ABx(x Ax B))
42, 3sylibr 137 1 (φAB)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1224   wcel 1370  wss 2890
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-11 1374  ax-4 1377  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000
This theorem depends on definitions:  df-bi 110  df-nf 1326  df-sb 1624  df-clab 2005  df-cleq 2011  df-clel 2014  df-in 2897  df-ss 2904
This theorem is referenced by:  sscon  3050  ssdif  3051  unss1  3085  ssrin  3135  eq0rdv  3234  uniss  3571  intss1  3600  intmin  3605  intssunim  3607  iunss1  3638  iinss1  3639  ss2iun  3642  ssiun  3669  ssiun2  3670  iinss  3678  iinss2  3679  trintssm  3840  sspwb  3922  tron  4064  ssorduni  4159  ordsson  4164  ordpwsucss  4223  xpsspw  4373  relop  4409  dmss  4457  dmcosseq  4526  ssrnres  4686  chfnrn  5199  ffnfv  5244  f1imass  5334  fo1stresm  5707  fo2ndresm  5708  fo2ndf  5767  reldmtpos  5786  smoiun  5834  tfrlemi14d  5864  qsss  6072  distrlem1prl  6415  distrlem1pru  6416  distrlem5prl  6419  distrlem5pru  6420  ltprordil  6422  ltexprlemfl  6440  ltexprlemrl  6441  ltexprlemfu  6442  ltexprlemru  6443  addcanprleml  6445  addcanprlemu  6446  recexprlem1ssl  6461  recexprlem1ssu  6462  recexprlemss1l  6463  recexprlemss1u  6464
  Copyright terms: Public domain W3C validator