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

Theorem ssopab2i 4729
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 4727 . 2  |-  ( A. x A. y ( ph  ->  ps )  ->  { <. x ,  y >.  |  ph }  C_  { <. x ,  y >.  |  ps } )
2 ssopab2i.1 . . 3  |-  ( ph  ->  ps )
32ax-gen 1677 . 2  |-  A. y
( ph  ->  ps )
41, 3mpg 1679 1  |-  { <. x ,  y >.  |  ph }  C_  { <. x ,  y >.  |  ps }
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1450    C_ wss 3390   {copab 4453
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-in 3397  df-ss 3404  df-opab 4455
This theorem is referenced by:  elopabran  4739  brab2a  4889  opabssxp  4914  funopab4  5624  ssoprab2i  6404  cardf2  8395  dfac3  8570  axdc2lem  8896  fpwwe2lem1  9074  canthwe  9094  trclublem  13134  fullfunc  15889  fthfunc  15890  isfull  15893  isfth  15897  ipoval  16478  ipolerval  16480  eqgfval  16943  2ndcctbss  20547  iscgrg  24636  ishpg  24880  nvss  26293  ajfval  26531  afsval  29560  cvmlift2lem12  30109  dicval  34815  areaquad  36172  relopabVD  37361  pthsfval  39915  spthsfval  39916  crctS  39971  cyclS  39972  eupths  40112
  Copyright terms: Public domain W3C validator