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 1669	. 2 |- A. y ( ph -> ps )
4	1, 3	mpg 1671	1 |- { <. x , y >. | ph } C_ { <. x , y >. | ps }

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