This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 }