Theorem equcom 2045

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

Syntax hints:   ↔ wb 209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807

This theorem is referenced by:  equcomd  2046  dvelimhw  2383  sb8v  2391  sb8f  2392  nfeqf1  2417  eu1  2644  reu7  3704  reu8  3705  dfdif3OLD  4081  issn  4801  disjxun  5111  copsexgw  5473  copsexgwOLD  5474  copsexg  5475  dfid4  5558  dfid3  5560  opeliunxp  5729  opeliun2xp  5730  cnvi  5872  dmi  5912  elidinxp  6047  opabresid  6053  asymref2  6118  intirr  6119  coi1  6265  cnvso  6290  iotaval2  6508  brprcneu  6872  brprcneuALT  6873  dffv2  6977  fvn0ssdmfun  7070  f1oiso  7350  fvmpopr2d  7573  fsplit  8112  poxp2  8139  poxp3  8146  qsid  8779  mapsnend  9033  marypha2lem2  9396  fiinfg  9461  dfac5lem2  10108  dfac5lem3  10109  kmlem15  10148  brdom7disj  10515  suplem2pr  11038  wloglei  11746  fimaxre  12159  arch  12501  dflt2  13173  hashgt12el  14459  hashge2el2dif  14517  summo  15768  tosso  18473  opsrtoslem1  22175  mamulid  22567  mpomatmul  22572  mattpos1  22582  scmatscm  22639  1marepvmarrepid  22701  ist1-3  23475  unisngl  23653  fmid  24086  tgphaus  24243  dscopn  24699  iundisj2  25677  dvlip  26121  ply1divmo  26262  addsrid  28123  mulsrid  28272  disjabrex  32868  disjabrexf  32869  iundisj2f  32876  iundisj2fi  33083  grplsm0l  33656  esplyfvaln  33909  ordtconnlem1  34259  dfdm5  36164  dfrn5  36165  dffun10  36303  elfuns  36304  dfiota3  36312  brimg  36326  dfrdg4  36342  nn0prpwlem  36722  bj-axseprep  37599  fvineqsneu  37945  wl-equsalcom  38086  wl-sb9v  38092  matunitlindflem2  38156  ref5  38858  dfsucmap3  39002  pmapglb  40434  polval2N  40570  diclspsn  41858  sn-iotalem  42882  eq0rabdioph  43399  ontric3g  44140  undmrnresiss  44222  relopabVD  45501  icheq  48100  ichexmpl1  48107  pgnbgreunbgrlem4  48773  itsclquadeu  49442  oppcendc  49681