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

Theorem equcomi 2024
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 2019 . 2 𝑥 = 𝑥
2 ax7 2023 . 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 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782
This theorem is referenced by:  equcom  2025  equcoms  2027  ax13dgen2  2142  sbequ2  2251  sbequ2OLD  2252  cbv2w  2358  cbv2  2424  cbv2h  2427  axc16i  2459  equvini  2478  equsb2  2531  vtoclgft  3528  axsepgfromrep  5177  rext  5318  soxp  7810  axextnd  10002  prodmo  15281  mpomatmul  21049  finminlem  33740  bj-ssbid2ALT  34070  axc11n11  34090  axc11n11r  34091  bj-cbv2hv  34195  ax6er  34232  bj-imdiridlem  34561  wl-axc11rc11  34942  poimirlem25  35044  axc11nfromc11  36184  aev-o  36189
  Copyright terms: Public domain W3C validator