Theorem equcom 2025

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

Syntax hints:   ↔ wb 209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782

This theorem is referenced by:  equcomd  2026  equsb3rOLD  2108  dvelimhw  2355  nfeqf1  2386  eu1  2671  reu7  3671  reu8  3672  dfdif3  4042  issn  4723  iunid  4947  disjxun  5028  copsexgw  5346  copsexg  5347  opelopabsbALT  5381  dfid4  5426  dfid3  5427  opeliunxp  5583  dmi  5755  elidinxp  5878  opabresid  5884  opabresidOLD  5886  asymref2  5944  intirr  5945  cnvi  5967  coi1  6082  cnvso  6107  iotaval  6298  brprcneu  6637  dffv2  6733  fvn0ssdmfun  6819  f1oiso  7083  fvmpopr2d  7290  fsplit  7795  qsid  8346  mapsnend  8571  marypha2lem2  8884  fiinfg  8947  dfac5lem2  9535  dfac5lem3  9536  kmlem15  9575  brdom7disj  9942  suplem2pr  10464  wloglei  11161  fimaxre  11573  arch  11882  dflt2  12529  hashgt12el  13779  hashge2el2dif  13834  summo  15066  tosso  17638  opsrtoslem1  20723  mamulid  21046  mpomatmul  21051  mattpos1  21061  scmatscm  21118  1marepvmarrepid  21180  ist1-3  21954  unisngl  22132  fmid  22565  tgphaus  22722  dscopn  23180  iundisj2  24153  dvlip  24596  ply1divmo  24736  disjabrex  30345  disjabrexf  30346  iundisj2f  30353  iundisj2fi  30546  ordtconnlem1  31277  dfdm5  33129  dfrn5  33130  dffun10  33488  elfuns  33489  dfiota3  33497  brimg  33511  dfrdg4  33525  nn0prpwlem  33783  fvineqsneu  34828  wl-equsalcom  34947  wl-dfralflem  35003  matunitlindflem2  35054  pmapglb  37066  polval2N  37202  diclspsn  38490  eq0rabdioph  39717  ontric3g  40230  undmrnresiss  40304  relopabVD  41607  icheq  43979  ichexmpl1  43986  opeliun2xp  44734  itsclquadeu  45191