Theorem equcom 2019

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 2018	. 2 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
2		equcomi 2018	. 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 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780

This theorem is referenced by:  equcomd  2020  dvelimhw  2339  sb8v  2346  sb8f  2347  nfeqf1  2376  eu1  2604  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  7352  fvmpopr2d  7573  fsplit  8107  poxp2  8133  poxp3  8140  qsid  8781  mapsnend  9040  marypha2lem2  9435  fiinfg  9498  dfac5lem2  10123  dfac5lem3  10124  kmlem15  10163  brdom7disj  10530  suplem2pr  11052  wloglei  11752  fimaxre  12164  arch  12475  dflt2  13133  hashgt12el  14388  hashge2el2dif  14447  summo  15669  tosso  18378  opsrtoslem1  21837  mamulid  22165  mpomatmul  22170  mattpos1  22180  scmatscm  22237  1marepvmarrepid  22299  ist1-3  23075  unisngl  23253  fmid  23686  tgphaus  23843  dscopn  24304  iundisj2  25300  dvlip  25744  ply1divmo  25887  addsrid  27684  mulsrid  27806  disjabrex  32078  disjabrexf  32079  iundisj2f  32086  iundisj2fi  32273  grplsm0l  32785  ordtconnlem1  33200  dfdm5  35046  dfrn5  35047  dffun10  35188  elfuns  35189  dfiota3  35197  brimg  35211  dfrdg4  35225  nn0prpwlem  35512  fvineqsneu  36597  wl-equsalcom  36716  matunitlindflem2  36790  ref5  37487  pmapglb  38946  polval2N  39082  diclspsn  40370  sn-iotalem  41346  eq0rabdioph  41818  ontric3g  42577  undmrnresiss  42659  relopabVD  43966  icheq  46430  ichexmpl1  46437  opeliun2xp  47098  itsclquadeu  47552