![]() |
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 2008 | . 2 ⊢ 𝑥 = 𝑥 | |
2 | ax7 2012 | . 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 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1776 |
This theorem is referenced by: equcom 2014 equcoms 2016 ax13dgen2 2135 sbequ2 2246 cbv2w 2337 cbv2 2405 cbv2h 2408 axc16i 2438 equvini 2457 equsb2 2494 axsepgfromrep 5299 rext 5458 dfid2 5584 soxp 8152 xpord3inddlem 8177 axextnd 10628 prodmo 15968 mpomatmul 22467 cbvex1v 35066 finminlem 36300 bj-ssbid2ALT 36645 axc11n11 36664 axc11n11r 36665 bj-cbv2hv 36779 ax6er 36815 bj-dfid2ALT 37047 bj-imdiridlem 37167 wl-axc11rc11 37563 poimirlem25 37631 axc11nfromc11 38907 aev-o 38912 |
Copyright terms: Public domain | W3C validator |