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

Theorem ssopab2i 4765
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 4763 . 2  |-  ( A. x A. y ( ph  ->  ps )  ->  { <. x ,  y >.  |  ph }  C_  { <. x ,  y >.  |  ps } )
2 ssopab2i.1 . . 3  |-  ( ph  ->  ps )
32ax-gen 1605 . 2  |-  A. y
( ph  ->  ps )
41, 3mpg 1607 1  |-  { <. x ,  y >.  |  ph }  C_  { <. x ,  y >.  |  ps }
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1381    C_ wss 3461   {copab 4494
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-in 3468  df-ss 3475  df-opab 4496
This theorem is referenced by:  brab2a  5039  opabssxp  5064  funopab4  5613  ssoprab2i  6376  cardf2  8327  dfac3  8505  axdc2lem  8831  fpwwe2lem1  9012  canthwe  9032  fullfunc  15149  fthfunc  15150  isfull  15153  isfth  15157  ipoval  15658  ipolerval  15660  eqgfval  16123  2ndcctbss  19829  iscgrg  23776  ishpg  24000  nvss  25358  ajfval  25596  afsval  28424  cvmlift2lem12  28632  areaquad  31160  relopabVD  33434  dicval  36643  trclubg  37478
  Copyright terms: Public domain W3C validator