![]() |
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 2016 | . 2 ⊢ 𝑥 = 𝑥 | |
2 | ax7 2020 | . 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 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 |
This theorem is referenced by: equcom 2022 equcoms 2024 ax13dgen2 2135 sbequ2 2242 cbv2w 2334 cbv2 2403 cbv2h 2406 axc16i 2436 equvini 2455 equsb2 2492 axsepgfromrep 5298 rext 5449 dfid2 5577 soxp 8115 xpord3inddlem 8140 axextnd 10586 prodmo 15880 mpomatmul 21948 finminlem 35203 bj-ssbid2ALT 35540 axc11n11 35560 axc11n11r 35561 bj-cbv2hv 35675 ax6er 35711 bj-dfid2ALT 35946 bj-imdiridlem 36066 wl-axc11rc11 36445 poimirlem25 36513 axc11nfromc11 37796 aev-o 37801 |
Copyright terms: Public domain | W3C validator |