Theorem dropab2

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	dropab2	|- ( A. x x = y -> { <. z , x >. | ph } = { <. z , y >. | ph } )

Proof

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