Theorem equcom 2051

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

This proof depends on syntax axioms:   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813

This theorem is used by:  equcomd  2052  dvelimhw  2375  sb8v  2383  sb8f  2384  nfeqf1  2409  eu1  2636  reu7  3690  reu8  3691  issn  4792  disjxun  5101  copsexgwOLD  5461  dfid4  5547  dfid3  5549  opeliunxp  5718  opeliun2xp  5719  cnvi  5863  dmi  5903  elidinxp  6036  opabresid  6042  asymref2  6111  intirr  6112  coi1  6264  cnvso  6291  iotaval2  6509  brprcneu  6875  brprcneuALT  6876  dffv2  6980  fvn0ssdmfun  7074  f1oiso  7359  fvmpopr2d  7582  fsplit  8128  poxp2  8160  poxp3  8167  qsid  8802  mapsnend  9064  marypha2lem2  9428  fiinfg  9493  dfac5lem2  10203  dfac5lem3  10204  kmlem15  10243  brdom7disj  10610  suplem2pr  11138  wloglei  11848  fimaxre  12261  arch  12603  dflt2  13277  hashgt12el  14567  hashge2el2dif  14625  summo  15883  tosso  18591  opsrtoslem1  22364  mamulid  22756  mpomatmul  22761  mattpos1  22771  scmatscm  22828  1marepvmarrepid  22890  matunitlindflem2  22995  ist1-3  23667  unisngl  23846  fmid  24279  tgphaus  24436  dscopn  24892  iundisj2  25870  dvlip  26313  ply1divmo  26454  addsrid  28350  mulsrid  28499  disjabrex  33176  disjabrexf  33177  iundisj2f  33184  iundisj2fi  33389  grplsm0l  33954  esplyfvaln  34206  ordtconnlem1  34556  dfdm5  36537  dfrn5  36538  dffun10  36676  elfuns  36677  dfiota3  36685  brimg  36699  dfrdg4  36715  nn0prpwlem  37110  bj-axseprep  37990  fvineqsneu  38334  wl-equsalcom  38475  wl-sb9v  38481  ref5  39251  dfsucmap3  39395  pmapglb  40827  polval2N  40963  diclspsn  42251  sn-iotalem  43275  eq0rabdioph  43786  ontric3g  44522  undmrnresiss  44603  relopabVD  45882  icheq  48543  ichexmpl1  48550  pgnbgreunbgrlem4  49216  itsclquadeu  49888  oppcendc  50125