Theorem fnopabeqd

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

	Ref	Expression
Hypothesis	fnopabeqd.1	$$⊢\phi \to B=C$$
Assertion	fnopabeqd	$$⊢\phi \to \left\{⟨x,y⟩|\left(x\in A\wedge y=B\right)\right\}=\left\{⟨x,y⟩|\left(x\in A\wedge y=C\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		fnopabeqd.1	$$⊢\phi \to B=C$$
2	1	eqeq2d	$$⊢\phi \to \left(y=B\leftrightarrow y=C\right)$$
3	2	anbi2d	$$⊢\phi \to \left(\left(x\in A\wedge y=B\right)\leftrightarrow \left(x\in A\wedge y=C\right)\right)$$
4	3	opabbidv	$$⊢\phi \to \left\{⟨x,y⟩|\left(x\in A\wedge y=B\right)\right\}=\left\{⟨x,y⟩|\left(x\in A\wedge y=C\right)\right\}$$