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

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

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