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

Metamath Proof Explorer

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 } )