Description: Equality deduction for function abstractions. (Contributed by Jeff Madsen, 19-Jun-2011)
Ref | Expression | ||
---|---|---|---|
Hypothesis | fnopabeqd.1 | ⊢ ( 𝜑 → 𝐵 = 𝐶 ) | |
Assertion | fnopabeqd | ⊢ ( 𝜑 → { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) } = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) } ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fnopabeqd.1 | ⊢ ( 𝜑 → 𝐵 = 𝐶 ) | |
2 | 1 | eqeq2d | ⊢ ( 𝜑 → ( 𝑦 = 𝐵 ↔ 𝑦 = 𝐶 ) ) |
3 | 2 | anbi2d | ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) ) ) |
4 | 3 | opabbidv | ⊢ ( 𝜑 → { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) } = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) } ) |