![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > equcomi | Structured version Visualization version GIF version |
Description: Commutative law for equality. Equality is a symmetric relation. Lemma 3 of [KalishMontague] p. 85. See also Lemma 7 of [Tarski] p. 69. (Contributed by NM, 10-Jan-1993.) (Revised by NM, 9-Apr-2017.) |
Ref | Expression |
---|---|
equcomi | ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | equid 2019 | . 2 ⊢ 𝑥 = 𝑥 | |
2 | ax7 2023 | . 2 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑥 → 𝑦 = 𝑥)) | |
3 | 1, 2 | mpi 20 | 1 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1782 |
This theorem is referenced by: equcom 2025 equcoms 2027 ax13dgen2 2139 sbequ2 2247 sbequ2OLD 2248 cbv2w 2346 cbv2 2412 cbv2h 2415 axc16i 2447 equvini 2466 equsb2 2510 vtoclgft 3501 axsepgfromrep 5165 rext 5306 soxp 7806 axextnd 10002 prodmo 15282 mpomatmul 21051 finminlem 33779 bj-ssbid2ALT 34109 axc11n11 34129 axc11n11r 34130 bj-cbv2hv 34234 ax6er 34271 bj-imdiridlem 34600 wl-axc11rc11 34980 poimirlem25 35082 axc11nfromc11 36222 aev-o 36227 |
Copyright terms: Public domain | W3C validator |