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

Theorem equcomi 1930
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 1925 . 2 𝑥 = 𝑥
2 ax7 1929 . 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 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695
This theorem is referenced by:  equcom  1931  equcoms  1933  ax13dgen2  2001  cbv2h  2255  axc11nOLD  2295  axc11nOLDOLD  2296  axc11nALT  2297  axc16i  2309  equsb2  2356  axsep  4702  rext  4837  iotaval  5765  soxp  7154  axextnd  9269  prodmo  14451  mpt2matmul  20013  finminlem  31288  bj-ssbid2ALT  31641  axc11n11  31665  axc11n11r  31666  bj-cbv2hv  31724  bj-axsep  31794  ax6er  31821  poimirlem25  32407  axc11nfromc11  33032  aev-o  33037
  Copyright terms: Public domain W3C validator