| 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 2011 | . 2 ⊢ 𝑥 = 𝑥 | |
| 2 | ax7 2015 | . 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 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 |
| This theorem is referenced by: equcom 2017 equcoms 2019 ax13dgen2 2138 sbequ2 2249 cbv2w 2339 cbv2 2408 cbv2h 2411 axc16i 2441 equvini 2460 equsb2 2497 axsepgfromrep 5294 rext 5453 dfid2 5580 soxp 8154 xpord3inddlem 8179 axextnd 10631 prodmo 15972 mpomatmul 22452 cbvex1v 35088 finminlem 36319 bj-ssbid2ALT 36664 axc11n11 36683 axc11n11r 36684 bj-cbv2hv 36798 ax6er 36834 bj-dfid2ALT 37066 bj-imdiridlem 37186 wl-axc11rc11 37584 poimirlem25 37652 axc11nfromc11 38927 aev-o 38932 oppcendc 48906 |
| Copyright terms: Public domain | W3C validator |