Theorem equcom 2100

Description: Commutative law for equality. Equality is a symmetric relation. (Contributed by NM, 20-Aug-1993.)

Assertion

Ref	Expression
equcom	⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥)

Proof of Theorem equcom

Step	Hyp	Ref	Expression
1		equcomi 2099	. 2 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
2		equcomi 2099	. 2 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑦)
3	1, 2	impbii 199	1 ⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥)

Syntax hints:   ↔ wb 196

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854

This theorem is referenced by:  equcomd  2101  dvelimhw  2318  nfeqf1  2444  eu1  2648  reu7  3542  reu8  3543  dfdif3  3863  issn  4508  iunid  4727  disjxun  4802  copsexg  5104  opelopabsbALT  5134  dfid3  5175  dfid4  5176  opeliunxp  5327  dmi  5495  opabresid  5613  restidsingOLD  5617  asymref2  5671  intirr  5672  cnvi  5695  coi1  5812  cnvso  5835  iotaval  6023  brprcneu  6345  dffv2  6433  fvn0ssdmfun  6513  f1oiso  6764  qsid  7980  mapsnen  8200  marypha2lem2  8507  fiinfg  8570  dfac5lem2  9137  dfac5lem3  9138  kmlem15  9178  brdom7disj  9545  suplem2pr  10067  wloglei  10752  fimaxre  11160  arch  11481  dflt2  12174  hashgt12el  13402  hashge2el2dif  13454  summo  14647  tosso  17237  opsrtoslem1  19686  mamulid  20449  mpt2matmul  20454  mattpos1  20464  scmatscm  20521  1marepvmarrepid  20583  ist1-3  21355  unisngl  21532  cnmptid  21666  fmid  21965  tgphaus  22121  dscopn  22579  iundisj2  23517  dvlip  23955  ply1divmo  24094  disjabrex  29702  disjabrexf  29703  iundisj2f  29710  iundisj2fi  29865  ordtconnlem1  30279  dfdm5  31981  dfrn5  31982  dffun10  32327  elfuns  32328  dfiota3  32336  brimg  32350  dfrdg4  32364  nn0prpwlem  32623  bj-ssbequ2  32949  wl-equsalcom  33641  matunitlindflem2  33719  pmapglb  35559  polval2N  35695  diclspsn  36985  eq0rabdioph  37842  undmrnresiss  38412  relopabVD  39636  mapsnend  39890  opeliun2xp  42621