Theorem oprabbi

Description: Equality deduction for class abstraction of nested ordered pairs. (Contributed by Giovanni Mascellani, 10-Apr-2018)

	Ref	Expression
Assertion	oprabbi	|- ( A. x A. y A. z ( ph <-> ps ) -> { <. <. x , y >. , z >. | ph } = { <. <. x , y >. , z >. | ps } )

Proof

Step	Hyp	Ref	Expression
1		eqoprab2b	|- ( { <. <. x , y >. , z >. | ph } = { <. <. x , y >. , z >. | ps } <-> A. x A. y A. z ( ph <-> ps ) )
2	1	biimpri	|- ( A. x A. y A. z ( ph <-> ps ) -> { <. <. x , y >. , z >. | ph } = { <. <. x , y >. , z >. | ps } )