Metamath Proof Explorer


Theorem fnopabeqd

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

Ref Expression
Hypothesis fnopabeqd.1 ( 𝜑𝐵 = 𝐶 )
Assertion fnopabeqd ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 = 𝐵 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 = 𝐶 ) } )

Proof

Step Hyp Ref Expression
1 fnopabeqd.1 ( 𝜑𝐵 = 𝐶 )
2 1 eqeq2d ( 𝜑 → ( 𝑦 = 𝐵𝑦 = 𝐶 ) )
3 2 anbi2d ( 𝜑 → ( ( 𝑥𝐴𝑦 = 𝐵 ) ↔ ( 𝑥𝐴𝑦 = 𝐶 ) ) )
4 3 opabbidv ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 = 𝐵 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 = 𝐶 ) } )