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 1669 . 2  |-  A. y
( ph  ->  ps )
41, 3mpg 1671 1  |-  { <. x ,  y >.  |  ph }  C_  { <. x ,  y >.  |  ps }
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1442    C_ wss 3404   {copab 4460
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-in 3411  df-ss 3418  df-opab 4462
This theorem is referenced by:  brab2a  4884  opabssxp  4909  funopab4  5617  ssoprab2i  6385  cardf2  8377  dfac3  8552  axdc2lem  8878  fpwwe2lem1  9056  canthwe  9076  trclublem  13059  fullfunc  15811  fthfunc  15812  isfull  15815  isfth  15819  ipoval  16400  ipolerval  16402  eqgfval  16865  2ndcctbss  20470  iscgrg  24557  ishpg  24801  nvss  26212  ajfval  26450  afsval  29488  cvmlift2lem12  30037  dicval  34744  areaquad  36101  relopabVD  37298
  Copyright terms: Public domain W3C validator