Theorem equcom 2018

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 2017	. 2 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
2		equcomi 2017	. 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 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008

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

This theorem is referenced by:  equcomd  2019  dvelimhw  2343  sb8v  2351  sb8f  2352  nfeqf1  2377  eu1  2603  reu7  3700  reu8  3701  dfdif3OLD  4077  issn  4792  iunidOLD  5020  disjxun  5100  copsexgw  5445  copsexg  5446  dfid4  5527  dfid3  5529  opeliunxp  5698  opeliun2xp  5699  dmi  5875  elidinxp  6004  opabresid  6010  asymref2  6078  intirr  6079  cnvi  6102  coi1  6223  cnvso  6249  iotaval2  6467  iotavalOLD  6473  brprcneu  6830  brprcneuALT  6831  dffv2  6938  fvn0ssdmfun  7028  f1oiso  7308  fvmpopr2d  7531  fsplit  8073  poxp2  8099  poxp3  8106  qsid  8731  mapsnend  8984  marypha2lem2  9363  fiinfg  9428  dfac5lem2  10053  dfac5lem3  10054  kmlem15  10094  brdom7disj  10460  suplem2pr  10982  wloglei  11686  fimaxre  12103  arch  12415  dflt2  13084  hashgt12el  14363  hashge2el2dif  14421  summo  15659  tosso  18358  opsrtoslem1  21995  mamulid  22361  mpomatmul  22366  mattpos1  22376  scmatscm  22433  1marepvmarrepid  22495  ist1-3  23269  unisngl  23447  fmid  23880  tgphaus  24037  dscopn  24494  iundisj2  25483  dvlip  25931  ply1divmo  26074  addsrid  27911  mulsrid  28056  disjabrex  32561  disjabrexf  32562  iundisj2f  32569  iundisj2fi  32770  grplsm0l  33367  ordtconnlem1  33907  dfdm5  35753  dfrn5  35754  dffun10  35895  elfuns  35896  dfiota3  35904  brimg  35918  dfrdg4  35932  nn0prpwlem  36303  fvineqsneu  37392  wl-equsalcom  37524  wl-sb9v  37530  matunitlindflem2  37604  ref5  38294  pmapglb  39757  polval2N  39893  diclspsn  41181  sn-iotalem  42202  eq0rabdioph  42757  ontric3g  43504  undmrnresiss  43586  relopabVD  44883  icheq  47456  ichexmpl1  47463  pgnbgreunbgrlem4  48102  itsclquadeu  48759  oppcendc  49000