Theorem dropab1

Description: Theorem to aid use of the distinctor reduction theorem with ordered pair class abstraction. (Contributed by Andrew Salmon, 25-Jul-2011)

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

Proof

Step	Hyp	Ref	Expression
1		opeq1	|- ( x = y -> <. x , z >. = <. y , z >. )
2	1	sps	|- ( A. x x = y -> <. x , z >. = <. y , z >. )
3	2	eqeq2d	|- ( A. x x = y -> ( w = <. x , z >. <-> w = <. y , z >. ) )
4	3	anbi1d	|- ( A. x x = y -> ( ( w = <. x , z >. /\ ph ) <-> ( w = <. y , z >. /\ ph ) ) )
5	4	drex2	|- ( A. x x = y -> ( E. z ( w = <. x , z >. /\ ph ) <-> E. z ( w = <. y , z >. /\ ph ) ) )
6	5	drex1	|- ( A. x x = y -> ( E. x E. z ( w = <. x , z >. /\ ph ) <-> E. y E. z ( w = <. y , z >. /\ ph ) ) )
7	6	abbidv	|- ( A. x x = y -> { w | E. x E. z ( w = <. x , z >. /\ ph ) } = { w | E. y E. z ( w = <. y , z >. /\ ph ) } )
8		df-opab	|- { <. x , z >. | ph } = { w | E. x E. z ( w = <. x , z >. /\ ph ) }
9		df-opab	|- { <. y , z >. | ph } = { w | E. y E. z ( w = <. y , z >. /\ ph ) }
10	7 8 9	3eqtr4g	|- ( A. x x = y -> { <. x , z >. | ph } = { <. y , z >. | ph } )