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

Theorem equcomi 1942
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 1937 . 2 𝑥 = 𝑥
2 ax7 1941 . 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 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1703
This theorem is referenced by:  equcom  1943  equcoms  1945  ax13dgen2  2013  cbv2h  2267  axc11nOLD  2306  axc11nOLDOLD  2307  axc11nALT  2308  axc16i  2320  equsb2  2367  axsep  4771  rext  4907  soxp  7275  axextnd  9398  prodmo  14647  mpt2matmul  20233  finminlem  32287  bj-ssbid2ALT  32621  axc11n11  32647  axc11n11r  32648  bj-cbv2hv  32706  bj-axsep  32768  ax6er  32795  poimirlem25  33405  axc11nfromc11  34030  aev-o  34035
  Copyright terms: Public domain W3C validator