Step |
Hyp |
Ref |
Expression |
1 |
|
cbvmpov.1 |
⊢ ( 𝑥 = 𝑧 → 𝐶 = 𝐸 ) |
2 |
|
cbvmpov.2 |
⊢ ( 𝑦 = 𝑤 → 𝐸 = 𝐷 ) |
3 |
|
eleq1w |
⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) ) |
4 |
|
eleq1w |
⊢ ( 𝑦 = 𝑤 → ( 𝑦 ∈ 𝐵 ↔ 𝑤 ∈ 𝐵 ) ) |
5 |
3 4
|
bi2anan9 |
⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ) ) |
6 |
1 2
|
sylan9eq |
⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → 𝐶 = 𝐷 ) |
7 |
6
|
eqeq2d |
⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝑣 = 𝐶 ↔ 𝑣 = 𝐷 ) ) |
8 |
5 7
|
anbi12d |
⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑣 = 𝐶 ) ↔ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑣 = 𝐷 ) ) ) |
9 |
8
|
cbvoprab12v |
⊢ { 〈 〈 𝑥 , 𝑦 〉 , 𝑣 〉 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑣 = 𝐶 ) } = { 〈 〈 𝑧 , 𝑤 〉 , 𝑣 〉 ∣ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑣 = 𝐷 ) } |
10 |
|
df-mpo |
⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = { 〈 〈 𝑥 , 𝑦 〉 , 𝑣 〉 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑣 = 𝐶 ) } |
11 |
|
df-mpo |
⊢ ( 𝑧 ∈ 𝐴 , 𝑤 ∈ 𝐵 ↦ 𝐷 ) = { 〈 〈 𝑧 , 𝑤 〉 , 𝑣 〉 ∣ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑣 = 𝐷 ) } |
12 |
9 10 11
|
3eqtr4i |
⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑧 ∈ 𝐴 , 𝑤 ∈ 𝐵 ↦ 𝐷 ) |