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

Theorem ss2abi 3169
Description: Inference of abstraction subclass from implication. (Contributed by NM, 31-Mar-1995.)
Hypothesis
Ref Expression
ss2abi.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
ss2abi  |-  { x  |  ph }  C_  { x  |  ps }

Proof of Theorem ss2abi
StepHypRef Expression
1 ss2ab 3165 . 2  |-  ( { x  |  ph }  C_ 
{ x  |  ps } 
<-> 
A. x ( ph  ->  ps ) )
2 ss2abi.1 . 2  |-  ( ph  ->  ps )
31, 2mpgbir 1429 1  |-  { x  |  ph }  C_  { x  |  ps }
Colors of variables: wff set class
Syntax hints:    -> wi 4   {cab 2125    C_ 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-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  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-nfc 2270  df-in 3077  df-ss 3084
This theorem is referenced by:  abssi  3172  rabssab  3184  pwsnss  3730  iinuniss  3895  pwpwssunieq  3901  abssexg  4106  imassrn  4892  imadiflem  5202  imainlem  5204  fabexg  5310  f1oabexg  5379  tfrcllemssrecs  6249  mapex  6548  tgval  12232  tgvalex  12233
  Copyright terms: Public domain W3C validator