Theorem equcom 2020

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

Syntax hints:   ↔ wb 206

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 1912  ax-6 1969  ax-7 2010

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782

This theorem is referenced by:  equcomd  2021  dvelimhw  2350  sb8v  2358  sb8f  2359  nfeqf1  2384  eu1  2611  reu7  3679  reu8  3680  dfdif3OLD  4059  issn  4776  disjxun  5084  copsexgw  5436  copsexg  5437  dfid4  5518  dfid3  5520  opeliunxp  5689  opeliun2xp  5690  dmi  5868  elidinxp  6001  opabresid  6007  asymref2  6072  intirr  6073  cnvi  6097  coi1  6219  cnvso  6244  iotaval2  6461  brprcneu  6822  brprcneuALT  6823  dffv2  6927  fvn0ssdmfun  7018  f1oiso  7297  fvmpopr2d  7520  fsplit  8058  poxp2  8084  poxp3  8091  qsid  8719  mapsnend  8974  marypha2lem2  9340  fiinfg  9405  dfac5lem2  10035  dfac5lem3  10036  kmlem15  10076  brdom7disj  10442  suplem2pr  10965  wloglei  11670  fimaxre  12087  arch  12399  dflt2  13063  hashgt12el  14346  hashge2el2dif  14404  summo  15641  tosso  18341  opsrtoslem1  22011  mamulid  22384  mpomatmul  22389  mattpos1  22399  scmatscm  22456  1marepvmarrepid  22518  ist1-3  23292  unisngl  23470  fmid  23903  tgphaus  24060  dscopn  24516  iundisj2  25494  dvlip  25939  ply1divmo  26082  addsrid  27944  mulsrid  28093  disjabrex  32641  disjabrexf  32642  iundisj2f  32649  iundisj2fi  32860  grplsm0l  33468  esplyfvaln  33723  ordtconnlem1  34074  dfdm5  35961  dfrn5  35962  dffun10  36100  elfuns  36101  dfiota3  36109  brimg  36123  dfrdg4  36139  nn0prpwlem  36510  bj-axseprep  37379  fvineqsneu  37723  wl-equsalcom  37859  wl-sb9v  37865  matunitlindflem2  37929  ref5  38631  dfsucmap3  38775  pmapglb  40207  polval2N  40343  diclspsn  41631  sn-iotalem  42654  eq0rabdioph  43207  ontric3g  43952  undmrnresiss  44034  relopabVD  45330  icheq  47896  ichexmpl1  47903  pgnbgreunbgrlem4  48553  itsclquadeu  49211  oppcendc  49451