Theorem fnopabeqd

Description: Equality deduction for function abstractions. (Contributed by Jeff Madsen, 19-Jun-2011)

	Ref	Expression
Hypothesis	fnopabeqd.1	|- ( ph -> B = C )
Assertion	fnopabeqd	|- ( ph -> { <. x , y >. | ( x e. A /\ y = B ) } = { <. x , y >. | ( x e. A /\ y = C ) } )

Proof

Step	Hyp	Ref	Expression
1		fnopabeqd.1	|- ( ph -> B = C )
2	1	eqeq2d	|- ( ph -> ( y = B <-> y = C ) )
3	2	anbi2d	|- ( ph -> ( ( x e. A /\ y = B ) <-> ( x e. A /\ y = C ) ) )
4	3	opabbidv	|- ( ph -> { <. x , y >. | ( x e. A /\ y = B ) } = { <. x , y >. | ( x e. A /\ y = C ) } )