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 1926 | . 2 ⊢ 𝑥 = 𝑥 | |
2 | ax7 1930 | . 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 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 |
This theorem depends on definitions: df-bi 196 df-an 385 df-ex 1696 |
This theorem is referenced by: equcom 1932 equcoms 1934 ax13dgen2 2002 cbv2h 2257 axc11nOLD 2296 axc11nOLDOLD 2297 axc11nALT 2298 axc16i 2310 equsb2 2357 axsep 4708 rext 4843 iotaval 5779 soxp 7177 axextnd 9292 prodmo 14505 mpt2matmul 20071 finminlem 31482 bj-ssbid2ALT 31835 axc11n11 31859 axc11n11r 31860 bj-cbv2hv 31918 bj-axsep 31981 ax6er 32008 poimirlem25 32604 axc11nfromc11 33229 aev-o 33234 |
Copyright terms: Public domain | W3C validator |