Theorem ssopab2

Description: Equivalence of ordered pair abstraction subclass and implication. (Contributed by NM, 27-Dec-1996) (Revised by Mario Carneiro, 19-May-2013)

	Ref	Expression
Assertion	ssopab2	|- ( A. x A. y ( ph -> ps ) -> { <. x , y >. | ph } C_ { <. x , y >. | ps } )

Proof

Step	Hyp	Ref	Expression
1		id	|- ( ( ph -> ps ) -> ( ph -> ps ) )
2	1	anim2d	|- ( ( ph -> ps ) -> ( ( z = <. x , y >. /\ ph ) -> ( z = <. x , y >. /\ ps ) ) )
3	2	aleximi	|- ( A. y ( ph -> ps ) -> ( E. y ( z = <. x , y >. /\ ph ) -> E. y ( z = <. x , y >. /\ ps ) ) )
4	3	aleximi	|- ( A. x A. y ( ph -> ps ) -> ( E. x E. y ( z = <. x , y >. /\ ph ) -> E. x E. y ( z = <. x , y >. /\ ps ) ) )
5	4	ss2abdv	|- ( A. x A. y ( ph -> ps ) -> { z | E. x E. y ( z = <. x , y >. /\ ph ) } C_ { z | E. x E. y ( z = <. x , y >. /\ ps ) } )
6		df-opab	|- { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }
7		df-opab	|- { <. x , y >. | ps } = { z | E. x E. y ( z = <. x , y >. /\ ps ) }
8	5 6 7	3sstr4g	|- ( A. x A. y ( ph -> ps ) -> { <. x , y >. | ph } C_ { <. x , y >. | ps } )