Theorem ssopab2dv

Description: Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 19-Jan-2014) (Revised by Mario Carneiro, 24-Jun-2014)

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

Proof

Step	Hyp	Ref	Expression
1		ssopab2dv.1	|- ( ph -> ( ps -> ch ) )
2	1	alrimivv	|- ( ph -> A. x A. y ( ps -> ch ) )
3		ssopab2	|- ( A. x A. y ( ps -> ch ) -> { <. x , y >. | ps } C_ { <. x , y >. | ch } )
4	2 3	syl	|- ( ph -> { <. x , y >. | ps } C_ { <. x , y >. | ch } )