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

Theorem ssopab2i 4775
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 4773 . 2  |-  ( A. x A. y ( ph  ->  ps )  ->  { <. x ,  y >.  |  ph }  C_  { <. x ,  y >.  |  ps } )
2 ssopab2i.1 . . 3  |-  ( ph  ->  ps )
32ax-gen 1601 . 2  |-  A. y
( ph  ->  ps )
41, 3mpg 1603 1  |-  { <. x ,  y >.  |  ph }  C_  { <. x ,  y >.  |  ps }
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1377    C_ wss 3476   {copab 4504
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-in 3483  df-ss 3490  df-opab 4506
This theorem is referenced by:  brab2a  5049  opabssxp  5074  funopab4  5623  ssoprab2i  6376  cardf2  8325  dfac3  8503  axdc2lem  8829  fpwwe2lem1  9010  canthwe  9030  fullfunc  15136  fthfunc  15137  isfull  15140  isfth  15144  ipoval  15644  ipolerval  15646  eqgfval  16063  2ndcctbss  19762  iscgrg  23729  nvss  25259  ajfval  25497  afsval  28302  cvmlift2lem12  28510  areaquad  31016  relopabVD  32998  dicval  36190  trclubg  37012
  Copyright terms: Public domain W3C validator