Step |
Hyp |
Ref |
Expression |
1 |
|
cbvoprab3v.1 |
⊢ ( 𝑧 = 𝑤 → ( 𝜑 ↔ 𝜓 ) ) |
2 |
|
opeq2 |
⊢ ( 𝑧 = 𝑤 → 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 = 〈 〈 𝑥 , 𝑦 〉 , 𝑤 〉 ) |
3 |
2
|
eqeq2d |
⊢ ( 𝑧 = 𝑤 → ( 𝑣 = 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ↔ 𝑣 = 〈 〈 𝑥 , 𝑦 〉 , 𝑤 〉 ) ) |
4 |
3 1
|
anbi12d |
⊢ ( 𝑧 = 𝑤 → ( ( 𝑣 = 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∧ 𝜑 ) ↔ ( 𝑣 = 〈 〈 𝑥 , 𝑦 〉 , 𝑤 〉 ∧ 𝜓 ) ) ) |
5 |
4
|
cbvexvw |
⊢ ( ∃ 𝑧 ( 𝑣 = 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∧ 𝜑 ) ↔ ∃ 𝑤 ( 𝑣 = 〈 〈 𝑥 , 𝑦 〉 , 𝑤 〉 ∧ 𝜓 ) ) |
6 |
5
|
2exbii |
⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑣 = 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑤 ( 𝑣 = 〈 〈 𝑥 , 𝑦 〉 , 𝑤 〉 ∧ 𝜓 ) ) |
7 |
6
|
abbii |
⊢ { 𝑣 ∣ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑣 = 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∧ 𝜑 ) } = { 𝑣 ∣ ∃ 𝑥 ∃ 𝑦 ∃ 𝑤 ( 𝑣 = 〈 〈 𝑥 , 𝑦 〉 , 𝑤 〉 ∧ 𝜓 ) } |
8 |
|
df-oprab |
⊢ { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ 𝜑 } = { 𝑣 ∣ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑣 = 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∧ 𝜑 ) } |
9 |
|
df-oprab |
⊢ { 〈 〈 𝑥 , 𝑦 〉 , 𝑤 〉 ∣ 𝜓 } = { 𝑣 ∣ ∃ 𝑥 ∃ 𝑦 ∃ 𝑤 ( 𝑣 = 〈 〈 𝑥 , 𝑦 〉 , 𝑤 〉 ∧ 𝜓 ) } |
10 |
7 8 9
|
3eqtr4i |
⊢ { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ 𝜑 } = { 〈 〈 𝑥 , 𝑦 〉 , 𝑤 〉 ∣ 𝜓 } |