![]() |
Higher-Order Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > HOLE Home > Th. List > eqcomx | GIF version |
Description: Commutativity of equality. (Contributed by Mario Carneiro, 7-Oct-2014.) |
Ref | Expression |
---|---|
eqcomx.1 | ⊢ A:α |
eqcomx.2 | ⊢ B:α |
eqcomx.3 | ⊢ R⊧(( = A)B) |
Ref | Expression |
---|---|
eqcomx | ⊢ R⊧(( = B)A) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqcomx.3 | . . . 4 ⊢ R⊧(( = A)B) | |
2 | 1 | ax-cb1 29 | . . 3 ⊢ R:∗ |
3 | eqcomx.1 | . . . 4 ⊢ A:α | |
4 | 3 | ax-refl 42 | . . 3 ⊢ ⊤⊧(( = A)A) |
5 | 2, 4 | a1i 28 | . 2 ⊢ R⊧(( = A)A) |
6 | weq 41 | . . . . . 6 ⊢ = :(α → (α → ∗)) | |
7 | 6 | ax-refl 42 | . . . . 5 ⊢ ⊤⊧(( = = ) = ) |
8 | 2, 7 | a1i 28 | . . . 4 ⊢ R⊧(( = = ) = ) |
9 | eqcomx.2 | . . . . 5 ⊢ B:α | |
10 | 6, 6, 3, 9 | ax-ceq 51 | . . . 4 ⊢ ((( = = ) = ), (( = A)B))⊧(( = ( = A))( = B)) |
11 | 8, 1, 10 | syl2anc 19 | . . 3 ⊢ R⊧(( = ( = A))( = B)) |
12 | 6, 3 | wc 50 | . . . 4 ⊢ ( = A):(α → ∗) |
13 | 6, 9 | wc 50 | . . . 4 ⊢ ( = B):(α → ∗) |
14 | 12, 13, 3, 3 | ax-ceq 51 | . . 3 ⊢ ((( = ( = A))( = B)), (( = A)A))⊧(( = (( = A)A))(( = B)A)) |
15 | 11, 5, 14 | syl2anc 19 | . 2 ⊢ R⊧(( = (( = A)A))(( = B)A)) |
16 | 5, 15 | ax-eqmp 45 | 1 ⊢ R⊧(( = B)A) |
Colors of variables: type var term |
Syntax hints: → ht 2 ∗hb 3 kc 5 = ke 7 ⊧wffMMJ2 11 wffMMJ2t 12 |
This theorem was proved from axioms: ax-syl 15 ax-jca 17 ax-trud 26 ax-cb1 29 ax-weq 40 ax-refl 42 ax-eqmp 45 ax-wc 49 ax-ceq 51 |
This theorem is referenced by: mpbirx 53 eqcomi 79 |
Copyright terms: Public domain | W3C validator |