Step |
Hyp |
Ref |
Expression |
1 |
|
ffnafv |
⊢ ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ↔ ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ ∀ 𝑤 ∈ ( 𝐴 × 𝐵 ) ( 𝐹 ''' 𝑤 ) ∈ 𝐶 ) ) |
2 |
|
afveq2 |
⊢ ( 𝑤 = 〈 𝑥 , 𝑦 〉 → ( 𝐹 ''' 𝑤 ) = ( 𝐹 ''' 〈 𝑥 , 𝑦 〉 ) ) |
3 |
|
df-aov |
⊢ (( 𝑥 𝐹 𝑦 )) = ( 𝐹 ''' 〈 𝑥 , 𝑦 〉 ) |
4 |
2 3
|
eqtr4di |
⊢ ( 𝑤 = 〈 𝑥 , 𝑦 〉 → ( 𝐹 ''' 𝑤 ) = (( 𝑥 𝐹 𝑦 )) ) |
5 |
4
|
eleq1d |
⊢ ( 𝑤 = 〈 𝑥 , 𝑦 〉 → ( ( 𝐹 ''' 𝑤 ) ∈ 𝐶 ↔ (( 𝑥 𝐹 𝑦 )) ∈ 𝐶 ) ) |
6 |
5
|
ralxp |
⊢ ( ∀ 𝑤 ∈ ( 𝐴 × 𝐵 ) ( 𝐹 ''' 𝑤 ) ∈ 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 (( 𝑥 𝐹 𝑦 )) ∈ 𝐶 ) |
7 |
6
|
anbi2i |
⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ ∀ 𝑤 ∈ ( 𝐴 × 𝐵 ) ( 𝐹 ''' 𝑤 ) ∈ 𝐶 ) ↔ ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 (( 𝑥 𝐹 𝑦 )) ∈ 𝐶 ) ) |
8 |
1 7
|
bitri |
⊢ ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ↔ ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 (( 𝑥 𝐹 𝑦 )) ∈ 𝐶 ) ) |