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

Theorem equcomi 2021
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 2016 . 2 𝑥 = 𝑥
2 ax7 2020 . 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 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783
This theorem is referenced by:  equcom  2022  equcoms  2024  ax13dgen2  2135  sbequ2  2242  cbv2w  2334  cbv2  2403  cbv2h  2406  axc16i  2436  equvini  2455  equsb2  2492  axsepgfromrep  5298  rext  5449  dfid2  5577  soxp  8115  xpord3inddlem  8140  axextnd  10586  prodmo  15880  mpomatmul  21948  finminlem  35203  bj-ssbid2ALT  35540  axc11n11  35560  axc11n11r  35561  bj-cbv2hv  35675  ax6er  35711  bj-dfid2ALT  35946  bj-imdiridlem  36066  wl-axc11rc11  36445  poimirlem25  36513  axc11nfromc11  37796  aev-o  37801
  Copyright terms: Public domain W3C validator