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

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

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