Description: Rule used to change the third bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 8-Oct-2004) (Revised by David Abernethy, 19-Jun-2012)
Ref | Expression | ||
---|---|---|---|
Hypothesis | cbvoprab3v.1 | ⊢ ( 𝑧 = 𝑤 → ( 𝜑 ↔ 𝜓 ) ) | |
Assertion | cbvoprab3v | ⊢ { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ 𝜑 } = { 〈 〈 𝑥 , 𝑦 〉 , 𝑤 〉 ∣ 𝜓 } |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbvoprab3v.1 | ⊢ ( 𝑧 = 𝑤 → ( 𝜑 ↔ 𝜓 ) ) | |
2 | nfv | ⊢ Ⅎ 𝑤 𝜑 | |
3 | nfv | ⊢ Ⅎ 𝑧 𝜓 | |
4 | 2 3 1 | cbvoprab3 | ⊢ { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ 𝜑 } = { 〈 〈 𝑥 , 𝑦 〉 , 𝑤 〉 ∣ 𝜓 } |