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

Theorem equcomi 1893
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 1887 . 2 𝑥 = 𝑥
2 ax7 1892 . 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 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883
This theorem depends on definitions:  df-bi 192  df-an 380  df-ex 1693
This theorem is referenced by:  equcom  1894  equcoms  1896  ax13dgen2  1962  cbv2h  2159  axc11n  2191  axc11nOLD  2192  axc11nALT  2193  axc16i  2205  equsb2  2252  axsep  4557  rext  4689  iotaval  5608  soxp  6988  axextnd  9101  prodmo  14150  mpt2matmul  19629  finminlem  31123  bj-ssbid2ALT  31441  bj-cbv2hv  31519  bj-axc11nv  31535  bj-axsep  31590  ax6er  31617  poimirlem25  32203  aecom-o  32704  axc11nfromc11  32730  aev-o  32735
  Copyright terms: Public domain W3C validator