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

Theorem equcomi 2016
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 2011 . 2 𝑥 = 𝑥
2 ax7 2015 . 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 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780
This theorem is referenced by:  equcom  2017  equcoms  2019  ax13dgen2  2138  sbequ2  2249  cbv2w  2339  cbv2  2408  cbv2h  2411  axc16i  2441  equvini  2460  equsb2  2497  axsepgfromrep  5294  rext  5453  dfid2  5580  soxp  8154  xpord3inddlem  8179  axextnd  10631  prodmo  15972  mpomatmul  22452  cbvex1v  35088  finminlem  36319  bj-ssbid2ALT  36664  axc11n11  36683  axc11n11r  36684  bj-cbv2hv  36798  ax6er  36834  bj-dfid2ALT  37066  bj-imdiridlem  37186  wl-axc11rc11  37584  poimirlem25  37652  axc11nfromc11  38927  aev-o  38932  oppcendc  48906
  Copyright terms: Public domain W3C validator