Theorem equcom 1932

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 1931	. 2 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
2		equcomi 1931	. 2 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑦)
3	1, 2	impbii 198	1 ⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥)

Syntax hints:   ↔ wb 195

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696

This theorem is referenced by:  equcomd  1933  equequ2OLD  1942  dvelimhw  2159  nfeqf1  2287  eu1  2498  reu7  3368  reu8  3369  issn  4303  iunid  4511  disjxun  4581  copsexg  4882  opelopabsbALT  4909  dfid3  4954  dfid4  4955  opeliunxp  5093  dmi  5261  opabresid  5374  restidsingOLD  5378  asymref2  5432  intirr  5433  cnvi  5456  coi1  5568  cnvso  5591  brprcneu  6096  dffv2  6181  fvn0ssdmfun  6258  f1oiso  6501  qsid  7700  mapsnen  7920  marypha2lem2  8225  fiinfg  8288  dfac5lem2  8830  dfac5lem3  8831  kmlem15  8869  brdom7disj  9234  suplem2pr  9754  wloglei  10439  fimaxre  10847  arch  11166  dflt2  11857  hashgt12el  13070  hashge2el2dif  13117  summo  14295  tosso  16859  opsrtoslem1  19305  mamulid  20066  mpt2matmul  20071  mattpos1  20081  scmatscm  20138  1marepvmarrepid  20200  ist1-3  20963  unisngl  21140  cnmptid  21274  fmid  21574  tgphaus  21730  dscopn  22188  iundisj2  23124  dvlip  23560  ply1divmo  23699  frg2wot1  26584  disjabrex  28777  disjabrexf  28778  iundisj2f  28785  iundisj2fi  28943  ordtconlem1  29298  dfdm5  30921  dfrn5  30922  dffun10  31191  elfuns  31192  dfiota3  31200  brimg  31214  dfrdg4  31228  nn0prpwlem  31487  bj-ssbequ2  31832  wl-equsalcom  32507  matunitlindflem2  32576  pmapglb  34074  polval2N  34210  diclspsn  35501  eq0rabdioph  36358  undmrnresiss  36929  relopabVD  38159  mapsnend  38386  frgr2wwlk1  41494  opeliun2xp  41904