Step |
Hyp |
Ref |
Expression |
1 |
|
eqfnfv2 |
⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐺 Fn ( 𝐶 × 𝐷 ) ) → ( 𝐹 = 𝐺 ↔ ( ( 𝐴 × 𝐵 ) = ( 𝐶 × 𝐷 ) ∧ ∀ 𝑧 ∈ ( 𝐴 × 𝐵 ) ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) ) ) |
2 |
|
fveq2 |
⊢ ( 𝑧 = 〈 𝑥 , 𝑦 〉 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 〈 𝑥 , 𝑦 〉 ) ) |
3 |
|
fveq2 |
⊢ ( 𝑧 = 〈 𝑥 , 𝑦 〉 → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 〈 𝑥 , 𝑦 〉 ) ) |
4 |
2 3
|
eqeq12d |
⊢ ( 𝑧 = 〈 𝑥 , 𝑦 〉 → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ↔ ( 𝐹 ‘ 〈 𝑥 , 𝑦 〉 ) = ( 𝐺 ‘ 〈 𝑥 , 𝑦 〉 ) ) ) |
5 |
|
df-ov |
⊢ ( 𝑥 𝐹 𝑦 ) = ( 𝐹 ‘ 〈 𝑥 , 𝑦 〉 ) |
6 |
|
df-ov |
⊢ ( 𝑥 𝐺 𝑦 ) = ( 𝐺 ‘ 〈 𝑥 , 𝑦 〉 ) |
7 |
5 6
|
eqeq12i |
⊢ ( ( 𝑥 𝐹 𝑦 ) = ( 𝑥 𝐺 𝑦 ) ↔ ( 𝐹 ‘ 〈 𝑥 , 𝑦 〉 ) = ( 𝐺 ‘ 〈 𝑥 , 𝑦 〉 ) ) |
8 |
4 7
|
bitr4di |
⊢ ( 𝑧 = 〈 𝑥 , 𝑦 〉 → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ↔ ( 𝑥 𝐹 𝑦 ) = ( 𝑥 𝐺 𝑦 ) ) ) |
9 |
8
|
ralxp |
⊢ ( ∀ 𝑧 ∈ ( 𝐴 × 𝐵 ) ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐹 𝑦 ) = ( 𝑥 𝐺 𝑦 ) ) |
10 |
9
|
anbi2i |
⊢ ( ( ( 𝐴 × 𝐵 ) = ( 𝐶 × 𝐷 ) ∧ ∀ 𝑧 ∈ ( 𝐴 × 𝐵 ) ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) ↔ ( ( 𝐴 × 𝐵 ) = ( 𝐶 × 𝐷 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐹 𝑦 ) = ( 𝑥 𝐺 𝑦 ) ) ) |
11 |
1 10
|
bitrdi |
⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐺 Fn ( 𝐶 × 𝐷 ) ) → ( 𝐹 = 𝐺 ↔ ( ( 𝐴 × 𝐵 ) = ( 𝐶 × 𝐷 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐹 𝑦 ) = ( 𝑥 𝐺 𝑦 ) ) ) ) |