Metamath Proof Explorer
Description: Rule used to change bound variables in an ordered-pair class
abstraction, using implicit substitution. (Contributed by NM, 15-Oct-1996)
|
|
Ref |
Expression |
|
Hypothesis |
cbvopabv.1 |
⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝜑 ↔ 𝜓 ) ) |
|
Assertion |
cbvopabv |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } = { 〈 𝑧 , 𝑤 〉 ∣ 𝜓 } |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
cbvopabv.1 |
⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝜑 ↔ 𝜓 ) ) |
2 |
|
nfv |
⊢ Ⅎ 𝑧 𝜑 |
3 |
|
nfv |
⊢ Ⅎ 𝑤 𝜑 |
4 |
|
nfv |
⊢ Ⅎ 𝑥 𝜓 |
5 |
|
nfv |
⊢ Ⅎ 𝑦 𝜓 |
6 |
2 3 4 5 1
|
cbvopab |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } = { 〈 𝑧 , 𝑤 〉 ∣ 𝜓 } |