Theorem equcom 2022

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

Syntax hints:   ↔ wb 205

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783

This theorem is referenced by:  equcomd  2023  dvelimhw  2344  sb8v  2351  sb8f  2352  nfeqf1  2380  eu1  2613  reu7  3668  reu8  3669  dfdif3  4050  issn  4764  iunid  4991  disjxun  5073  copsexgw  5405  copsexg  5406  dfid4  5491  dfid3  5493  opeliunxp  5655  dmi  5833  elidinxp  5954  opabresid  5960  opabresidOLD  5962  asymref2  6027  intirr  6028  cnvi  6050  coi1  6170  cnvso  6195  iotaval  6411  brprcneu  6773  brprcneuALT  6774  dffv2  6872  fvn0ssdmfun  6961  f1oiso  7231  fvmpopr2d  7443  fsplit  7966  qsid  8581  mapsnend  8835  marypha2lem2  9204  fiinfg  9267  dfac5lem2  9889  dfac5lem3  9890  kmlem15  9929  brdom7disj  10296  suplem2pr  10818  wloglei  11516  fimaxre  11928  arch  12239  dflt2  12891  hashgt12el  14146  hashge2el2dif  14203  summo  15438  tosso  18146  opsrtoslem1  21271  mamulid  21599  mpomatmul  21604  mattpos1  21614  scmatscm  21671  1marepvmarrepid  21733  ist1-3  22509  unisngl  22687  fmid  23120  tgphaus  23277  dscopn  23738  iundisj2  24722  dvlip  25166  ply1divmo  25309  disjabrex  30930  disjabrexf  30931  iundisj2f  30938  iundisj2fi  31127  grplsm0l  31600  ordtconnlem1  31883  dfdm5  33756  dfrn5  33757  poxp2  33799  poxp3  33805  xpord3ind  33809  addsid1  34136  dffun10  34225  elfuns  34226  dfiota3  34234  brimg  34248  dfrdg4  34262  nn0prpwlem  34520  fvineqsneu  35591  wl-equsalcom  35710  matunitlindflem2  35783  pmapglb  37791  polval2N  37927  diclspsn  39215  sn-iotalem  40196  iotavallem  40199  eq0rabdioph  40605  ontric3g  41136  undmrnresiss  41219  relopabVD  42528  icheq  44925  ichexmpl1  44932  opeliun2xp  45679  itsclquadeu  46134