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