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

Step	Hyp	Ref	Expression
1		ssopab2 4773	. 2 |- ( A. x A. y ( ph -> ps ) -> { <. x , y >. | ph } C_ { <. x , y >. | ps } )
2		ssopab2i.1	. . 3 |- ( ph -> ps )
3	2	ax-gen 1601	. 2 |- A. y ( ph -> ps )
4	1, 3	mpg 1603	1 |- { <. x , y >. | ph } C_ { <. x , y >. | ps }

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