Description: The alternative value of the operation on an ordered pair equals the operation's value on this ordered pair. (Contributed by Alexander van der Vekens, 26-May-2017)
Ref | Expression | ||
---|---|---|---|
Assertion | aovvoveq | ⊢ ( (( 𝐴 𝐹 𝐵 )) ∈ 𝐶 → (( 𝐴 𝐹 𝐵 )) = ( 𝐴 𝐹 𝐵 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-aov | ⊢ (( 𝐴 𝐹 𝐵 )) = ( 𝐹 ''' 〈 𝐴 , 𝐵 〉 ) | |
2 | 1 | eleq1i | ⊢ ( (( 𝐴 𝐹 𝐵 )) ∈ 𝐶 ↔ ( 𝐹 ''' 〈 𝐴 , 𝐵 〉 ) ∈ 𝐶 ) |
3 | afvvfveq | ⊢ ( ( 𝐹 ''' 〈 𝐴 , 𝐵 〉 ) ∈ 𝐶 → ( 𝐹 ''' 〈 𝐴 , 𝐵 〉 ) = ( 𝐹 ‘ 〈 𝐴 , 𝐵 〉 ) ) | |
4 | df-ov | ⊢ ( 𝐴 𝐹 𝐵 ) = ( 𝐹 ‘ 〈 𝐴 , 𝐵 〉 ) | |
5 | 3 1 4 | 3eqtr4g | ⊢ ( ( 𝐹 ''' 〈 𝐴 , 𝐵 〉 ) ∈ 𝐶 → (( 𝐴 𝐹 𝐵 )) = ( 𝐴 𝐹 𝐵 ) ) |
6 | 2 5 | sylbi | ⊢ ( (( 𝐴 𝐹 𝐵 )) ∈ 𝐶 → (( 𝐴 𝐹 𝐵 )) = ( 𝐴 𝐹 𝐵 ) ) |