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  2379  sb8v  2387  sb8f  2388  nfeqf1  2413  eu1  2640  reu7  3697  reu8  3698  issn  4799  disjxun  5109  copsexgw  5474  copsexgwOLD  5475  copsexg  5476  dfid4  5559  dfid3  5561  opeliunxp  5730  opeliun2xp  5731  cnvi  5873  dmi  5913  elidinxp  6048  opabresid  6054  asymref2  6119  intirr  6120  coi1  6266  cnvso  6293  iotaval2  6511  brprcneu  6875  brprcneuALT  6876  dffv2  6980  fvn0ssdmfun  7073  f1oiso  7358  fvmpopr2d  7581  fsplit  8118  poxp2  8145  poxp3  8152  qsid  8785  mapsnend  9040  marypha2lem2  9403  fiinfg  9468  dfac5lem2  10124  dfac5lem3  10125  kmlem15  10164  brdom7disj  10530  suplem2pr  11055  wloglei  11763  fimaxre  12176  arch  12518  dflt2  13191  hashgt12el  14479  hashge2el2dif  14537  summo  15793  tosso  18497  opsrtoslem1  22258  mamulid  22650  mpomatmul  22655  mattpos1  22665  scmatscm  22722  1marepvmarrepid  22784  ist1-3  23558  unisngl  23737  fmid  24170  tgphaus  24327  dscopn  24783  iundisj2  25761  dvlip  26205  ply1divmo  26346  addsrid  28210  mulsrid  28359  disjabrex  33000  disjabrexf  33001  iundisj2f  33008  iundisj2fi  33214  grplsm0l  33778  esplyfvaln  34030  ordtconnlem1  34380  dfdm5  36304  dfrn5  36305  dffun10  36443  elfuns  36444  dfiota3  36452  brimg  36466  dfrdg4  36482  nn0prpwlem  36892  bj-axseprep  37770  fvineqsneu  38116  wl-equsalcom  38257  wl-sb9v  38263  matunitlindflem2  38327  ref5  39028  dfsucmap3  39172  pmapglb  40604  polval2N  40740  diclspsn  42028  sn-iotalem  43052  eq0rabdioph  43567  ontric3g  44308  undmrnresiss  44390  relopabVD  45669  icheq  48271  ichexmpl1  48278  pgnbgreunbgrlem4  48944  itsclquadeu  49616  oppcendc  49855