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 2018 | . 2 ⊢ 𝑥 = 𝑥 | |
2 | ax7 2022 | . 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 1969 ax-7 2014 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1780 |
This theorem is referenced by: equcom 2024 equcoms 2026 ax13dgen2 2141 sbequ2 2249 sbequ2OLD 2250 cbv2w 2356 cbv2 2422 cbv2h 2425 axc16i 2457 equvini 2476 equsb2 2530 vtoclgft 3556 axsepgfromrep 5204 rext 5344 soxp 7826 axextnd 10016 prodmo 15293 mpomatmul 21058 finminlem 33670 bj-ssbid2ALT 34000 axc11n11 34020 axc11n11r 34021 bj-cbv2hv 34123 ax6er 34160 wl-axc11rc11 34819 poimirlem25 34921 axc11nfromc11 36066 aev-o 36071 |
Copyright terms: Public domain | W3C validator |