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

Theorem equcomi 1946
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 1941 . 2 𝑥 = 𝑥
2 ax7 1945 . 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 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702
This theorem is referenced by:  equcom  1947  equcoms  1949  ax13dgen2  2017  cbv2h  2273  axc11nOLD  2312  axc11nOLDOLD  2313  axc11nALT  2314  axc16i  2326  equsb2  2373  axsep  4745  rext  4882  soxp  7236  axextnd  9358  prodmo  14586  mpt2matmul  20166  finminlem  31927  bj-ssbid2ALT  32261  axc11n11  32287  axc11n11r  32288  bj-cbv2hv  32346  bj-axsep  32409  ax6er  32436  poimirlem25  33033  axc11nfromc11  33658  aev-o  33663
  Copyright terms: Public domain W3C validator