Metamath Proof Explorer


Theorem ssoprab2i

Description: Inference of operation class abstraction subclass from implication. (Contributed by NM, 11-Nov-1995) (Revised by David Abernethy, 19-Jun-2012)

Ref Expression
Hypothesis ssoprab2i.1
|- ( ph -> ps )
Assertion ssoprab2i
|- { <. <. x , y >. , z >. | ph } C_ { <. <. x , y >. , z >. | ps }

Proof

Step Hyp Ref Expression
1 ssoprab2i.1
 |-  ( ph -> ps )
2 1 anim2i
 |-  ( ( w = <. x , y >. /\ ph ) -> ( w = <. x , y >. /\ ps ) )
3 2 2eximi
 |-  ( E. x E. y ( w = <. x , y >. /\ ph ) -> E. x E. y ( w = <. x , y >. /\ ps ) )
4 3 ssopab2i
 |-  { <. w , z >. | E. x E. y ( w = <. x , y >. /\ ph ) } C_ { <. w , z >. | E. x E. y ( w = <. x , y >. /\ ps ) }
5 dfoprab2
 |-  { <. <. x , y >. , z >. | ph } = { <. w , z >. | E. x E. y ( w = <. x , y >. /\ ph ) }
6 dfoprab2
 |-  { <. <. x , y >. , z >. | ps } = { <. w , z >. | E. x E. y ( w = <. x , y >. /\ ps ) }
7 4 5 6 3sstr4i
 |-  { <. <. x , y >. , z >. | ph } C_ { <. <. x , y >. , z >. | ps }