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

Theorem equcomi 2013
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 2008 . 2 𝑥 = 𝑥
2 ax7 2012 . 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 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776
This theorem is referenced by:  equcom  2014  equcoms  2016  ax13dgen2  2135  sbequ2  2246  cbv2w  2337  cbv2  2405  cbv2h  2408  axc16i  2438  equvini  2457  equsb2  2494  axsepgfromrep  5299  rext  5458  dfid2  5584  soxp  8152  xpord3inddlem  8177  axextnd  10628  prodmo  15968  mpomatmul  22467  cbvex1v  35066  finminlem  36300  bj-ssbid2ALT  36645  axc11n11  36664  axc11n11r  36665  bj-cbv2hv  36779  ax6er  36815  bj-dfid2ALT  37047  bj-imdiridlem  37167  wl-axc11rc11  37563  poimirlem25  37631  axc11nfromc11  38907  aev-o  38912
  Copyright terms: Public domain W3C validator