MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssopab2i Unicode version

Theorem ssopab2i 4308
Description: Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 5-Apr-1995.)
Hypothesis
Ref Expression
ssopab2i.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
ssopab2i  |-  { <. x ,  y >.  |  ph }  C_  { <. x ,  y >.  |  ps }

Proof of Theorem ssopab2i
StepHypRef Expression
1 ssopab2 4306 . 2  |-  ( A. x A. y ( ph  ->  ps )  ->  { <. x ,  y >.  |  ph }  C_  { <. x ,  y >.  |  ps } )
2 ssopab2i.1 . . 3  |-  ( ph  ->  ps )
32ax-gen 1536 . 2  |-  A. y
( ph  ->  ps )
41, 3mpg 1538 1  |-  { <. x ,  y >.  |  ph }  C_  { <. x ,  y >.  |  ps }
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1530    C_ wss 3165   {copab 4092
This theorem is referenced by:  brab2a  4754  opabssxp  4778  funopab4  5305  ssoprab2i  5952  cardf2  7592  dfac3  7764  axdc2lem  8090  fpwwe2lem1  8269  canthwe  8289  fullfunc  13796  fthfunc  13797  isfull  13800  isfth  13804  ipoval  14273  ipolerval  14275  eqgfval  14681  2ndcctbss  17197  nvss  21165  ajfval  21403  cvmlift2lem12  23860  inposet  25381  relopabVD  28993  dicval  31988
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-in 3172  df-ss 3179  df-opab 4094
  Copyright terms: Public domain W3C validator