Step |
Hyp |
Ref |
Expression |
1 |
|
caovcomg.1 |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 𝐹 𝑦 ) = ( 𝑦 𝐹 𝑥 ) ) |
2 |
1
|
ralrimivva |
⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 𝐹 𝑦 ) = ( 𝑦 𝐹 𝑥 ) ) |
3 |
|
oveq1 |
⊢ ( 𝑥 = 𝐴 → ( 𝑥 𝐹 𝑦 ) = ( 𝐴 𝐹 𝑦 ) ) |
4 |
|
oveq2 |
⊢ ( 𝑥 = 𝐴 → ( 𝑦 𝐹 𝑥 ) = ( 𝑦 𝐹 𝐴 ) ) |
5 |
3 4
|
eqeq12d |
⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 𝐹 𝑦 ) = ( 𝑦 𝐹 𝑥 ) ↔ ( 𝐴 𝐹 𝑦 ) = ( 𝑦 𝐹 𝐴 ) ) ) |
6 |
|
oveq2 |
⊢ ( 𝑦 = 𝐵 → ( 𝐴 𝐹 𝑦 ) = ( 𝐴 𝐹 𝐵 ) ) |
7 |
|
oveq1 |
⊢ ( 𝑦 = 𝐵 → ( 𝑦 𝐹 𝐴 ) = ( 𝐵 𝐹 𝐴 ) ) |
8 |
6 7
|
eqeq12d |
⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 𝐹 𝑦 ) = ( 𝑦 𝐹 𝐴 ) ↔ ( 𝐴 𝐹 𝐵 ) = ( 𝐵 𝐹 𝐴 ) ) ) |
9 |
5 8
|
rspc2v |
⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 𝐹 𝑦 ) = ( 𝑦 𝐹 𝑥 ) → ( 𝐴 𝐹 𝐵 ) = ( 𝐵 𝐹 𝐴 ) ) ) |
10 |
2 9
|
mpan9 |
⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ) → ( 𝐴 𝐹 𝐵 ) = ( 𝐵 𝐹 𝐴 ) ) |