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  6346  dffv2  6434  fvn0ssdmfun  6514  f1oiso  6765  qsid  7982  mapsnen  8202  marypha2lem2  8509  fiinfg  8572  dfac5lem2  9157  dfac5lem3  9158  kmlem15  9198  brdom7disj  9565  suplem2pr  10087  wloglei  10772  fimaxre  11180  arch  11501  dflt2  12194  hashgt12el  13422  hashge2el2dif  13474  summo  14667  tosso  17257  opsrtoslem1  19706  mamulid  20469  mpt2matmul  20474  mattpos1  20484  scmatscm  20541  1marepvmarrepid  20603  ist1-3  21375  unisngl  21552  cnmptid  21686  fmid  21985  tgphaus  22141  dscopn  22599  iundisj2  23537  dvlip  23975  ply1divmo  24114  disjabrex  29723  disjabrexf  29724  iundisj2f  29731  iundisj2fi  29886  ordtconnlem1  30300  dfdm5  32002  dfrn5  32003  dffun10  32348  elfuns  32349  dfiota3  32357  brimg  32371  dfrdg4  32385  nn0prpwlem  32644  bj-ssbequ2  32971  wl-equsalcom  33659  matunitlindflem2  33737  pmapglb  35577  polval2N  35713  diclspsn  37003  eq0rabdioph  37860  undmrnresiss  38430  relopabVD  39654  mapsnend  39908  opeliun2xp  42639