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 398  df-ex 1783

This theorem is referenced by:  equcomd  2023  dvelimhw  2342  sb8v  2349  sb8f  2350  nfeqf1  2379  eu1  2607  reu7  3729  reu8  3730  dfdif3  4115  issn  4834  iunidOLD  5065  disjxun  5147  copsexgw  5491  copsexg  5492  dfid4  5576  dfid3  5578  opeliunxp  5744  dmi  5922  elidinxp  6044  opabresid  6050  asymref2  6119  intirr  6120  cnvi  6142  coi1  6262  cnvso  6288  iotaval2  6512  iotavalOLD  6518  brprcneu  6882  brprcneuALT  6883  dffv2  6987  fvn0ssdmfun  7077  f1oiso  7348  fvmpopr2d  7569  fsplit  8103  poxp2  8129  poxp3  8136  qsid  8777  mapsnend  9036  marypha2lem2  9431  fiinfg  9494  dfac5lem2  10119  dfac5lem3  10120  kmlem15  10159  brdom7disj  10526  suplem2pr  11048  wloglei  11746  fimaxre  12158  arch  12469  dflt2  13127  hashgt12el  14382  hashge2el2dif  14441  summo  15663  tosso  18372  opsrtoslem1  21616  mamulid  21943  mpomatmul  21948  mattpos1  21958  scmatscm  22015  1marepvmarrepid  22077  ist1-3  22853  unisngl  23031  fmid  23464  tgphaus  23621  dscopn  24082  iundisj2  25066  dvlip  25510  ply1divmo  25653  addsrid  27450  mulsrid  27572  disjabrex  31844  disjabrexf  31845  iundisj2f  31852  iundisj2fi  32039  grplsm0l  32544  ordtconnlem1  32935  dfdm5  34775  dfrn5  34776  dffun10  34917  elfuns  34918  dfiota3  34926  brimg  34940  dfrdg4  34954  nn0prpwlem  35255  fvineqsneu  36340  wl-equsalcom  36459  matunitlindflem2  36533  ref5  37230  pmapglb  38689  polval2N  38825  diclspsn  40113  sn-iotalem  41086  eq0rabdioph  41562  ontric3g  42321  undmrnresiss  42403  relopabVD  43710  icheq  46178  ichexmpl1  46185  opeliun2xp  47056  itsclquadeu  47511