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 }