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

Theorem equcom 2018
Description: Commutative law for equality. Equality is a symmetric relation. (Contributed by NM, 20-Aug-1993.)
Assertion
Ref Expression
equcom (𝑥 = 𝑦𝑦 = 𝑥)

Proof of Theorem equcom
StepHypRef Expression
1 equcomi 2017 . 2 (𝑥 = 𝑦𝑦 = 𝑥)
2 equcomi 2017 . 2 (𝑦 = 𝑥𝑥 = 𝑦)
31, 2impbii 210 1 (𝑥 = 𝑦𝑦 = 𝑥)
Colors of variables: wff setvar class
Syntax hints:  wb 207
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774
This theorem is referenced by:  equcomd  2019  equsb3rOLD  2104  dvelimhw  2360  nfeqf1  2392  eu1  2693  reu7  3727  reu8  3728  dfdif3  4095  issn  4762  iunid  4981  disjxun  5061  copsexgw  5378  copsexg  5379  opelopabsbALT  5413  dfid4  5460  dfid3  5461  opeliunxp  5618  dmi  5790  elidinxp  5910  opabresid  5916  opabresidOLD  5918  asymref2  5976  intirr  5977  cnvi  5999  coi1  6114  cnvso  6138  iotaval  6328  brprcneu  6661  dffv2  6755  fvn0ssdmfun  6840  f1oiso  7098  fsplit  7808  qsid  8358  mapsnend  8582  marypha2lem2  8894  fiinfg  8957  dfac5lem2  9544  dfac5lem3  9545  kmlem15  9584  brdom7disj  9947  suplem2pr  10469  wloglei  11166  fimaxre  11578  fimaxreOLD  11579  arch  11888  dflt2  12536  hashgt12el  13778  hashge2el2dif  13833  summo  15069  tosso  17641  opsrtoslem1  20199  mamulid  20985  mpomatmul  20990  mattpos1  21000  scmatscm  21057  1marepvmarrepid  21119  ist1-3  21892  unisngl  22070  fmid  22503  tgphaus  22659  dscopn  23117  iundisj2  24084  dvlip  24524  ply1divmo  24663  disjabrex  30266  disjabrexf  30267  iundisj2f  30274  iundisj2fi  30452  ordtconnlem1  31072  dfdm5  32919  dfrn5  32920  dffun10  33278  elfuns  33279  dfiota3  33287  brimg  33301  dfrdg4  33315  nn0prpwlem  33573  fvineqsneu  34580  wl-equsalcom  34669  wl-dfralflem  34724  matunitlindflem2  34775  pmapglb  36792  polval2N  36928  diclspsn  38216  eq0rabdioph  39257  ontric3g  39772  undmrnresiss  39848  relopabVD  41119  icheq  43471  ichexmpl1  43482  opeliun2xp  44283  itsclquadeu  44666
  Copyright terms: Public domain W3C validator