MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  equcomi Structured version   Visualization version   GIF version

Theorem equcomi 1894
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.)
Assertion
Ref Expression
equcomi (𝑥 = 𝑦𝑦 = 𝑥)

Proof of Theorem equcomi
StepHypRef Expression
1 equid 1889 . 2 𝑥 = 𝑥
2 ax7 1893 . 2 (𝑥 = 𝑦 → (𝑥 = 𝑥𝑦 = 𝑥))
31, 2mpi 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 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695
This theorem is referenced by:  equcom  1895  equcoms  1897  ax13dgen2  1963  cbv2h  2160  axc11nOLD  2200  axc11nOLDOLD  2201  axc11nALT  2202  axc16i  2214  equsb2  2261  axsep  4606  rext  4741  iotaval  5669  soxp  7057  axextnd  9172  prodmo  14378  mpt2matmul  19978  finminlem  31321  bj-ssbid2ALT  31673  axc11n11  31697  axc11n11r  31698  bj-cbv2hv  31756  bj-axsep  31826  ax6er  31853  poimirlem25  32498  axc11nfromc11  33123  aev-o  33128
  Copyright terms: Public domain W3C validator