Theorem equcom 2021

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

Syntax hints:   ↔ wb 208

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777

This theorem is referenced by:  equcomd  2022  equsb3rOLD  2107  dvelimhw  2362  nfeqf1  2393  eu1  2690  reu7  3722  reu8  3723  dfdif3  4090  issn  4756  iunid  4976  disjxun  5056  copsexgw  5373  copsexg  5374  opelopabsbALT  5408  dfid4  5455  dfid3  5456  opeliunxp  5613  dmi  5785  elidinxp  5905  opabresid  5911  opabresidOLD  5913  asymref2  5971  intirr  5972  cnvi  5994  coi1  6109  cnvso  6133  iotaval  6323  brprcneu  6656  dffv2  6750  fvn0ssdmfun  6836  f1oiso  7098  fsplit  7806  qsid  8357  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  12535  hashgt12el  13777  hashge2el2dif  13832  summo  15068  tosso  17640  opsrtoslem1  20258  mamulid  21044  mpomatmul  21049  mattpos1  21059  scmatscm  21116  1marepvmarrepid  21178  ist1-3  21951  unisngl  22129  fmid  22562  tgphaus  22719  dscopn  23177  iundisj2  24144  dvlip  24584  ply1divmo  24723  disjabrex  30326  disjabrexf  30327  iundisj2f  30334  iundisj2fi  30514  ordtconnlem1  31162  dfdm5  33011  dfrn5  33012  dffun10  33370  elfuns  33371  dfiota3  33379  brimg  33393  dfrdg4  33407  nn0prpwlem  33665  fvineqsneu  34686  wl-equsalcom  34776  wl-dfralflem  34832  matunitlindflem2  34883  pmapglb  36900  polval2N  37036  diclspsn  38324  eq0rabdioph  39366  ontric3g  39881  undmrnresiss  39957  relopabVD  41228  icheq  43614  ichexmpl1  43625  opeliun2xp  44375  itsclquadeu  44758