Step |
Hyp |
Ref |
Expression |
1 |
|
mpteq12df.1 |
⊢ Ⅎ 𝑥 𝜑 |
2 |
|
mpteq12df.2 |
⊢ ( 𝜑 → 𝐴 = 𝐶 ) |
3 |
|
mpteq12df.3 |
⊢ ( 𝜑 → 𝐵 = 𝐷 ) |
4 |
|
nfv |
⊢ Ⅎ 𝑦 𝜑 |
5 |
2
|
eleq2d |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶 ) ) |
6 |
3
|
eqeq2d |
⊢ ( 𝜑 → ( 𝑦 = 𝐵 ↔ 𝑦 = 𝐷 ) ) |
7 |
5 6
|
anbi12d |
⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) ↔ ( 𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐷 ) ) ) |
8 |
1 4 7
|
opabbid |
⊢ ( 𝜑 → { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) } = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐷 ) } ) |
9 |
|
df-mpt |
⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) } |
10 |
|
df-mpt |
⊢ ( 𝑥 ∈ 𝐶 ↦ 𝐷 ) = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐷 ) } |
11 |
8 9 10
|
3eqtr4g |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐶 ↦ 𝐷 ) ) |