Theorem equcom 2053

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 2052	. 2 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
2		equcomi 2052	. 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 1945  ax-6 2002  ax-7 2043

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

This theorem is used by:  equcomd  2054  dvelimhw  2378  sb8v  2385  sb8f  2386  nfeqf1  2411  eu1  2638  reu7  3693  reu8  3694  issn  4792  disjxun  5106  copsexgwOLD  5468  dfid4  5554  dfid3  5556  opeliunxp  5725  opeliun2xp  5726  cnvi  5875  dmi  5915  elidinxp  6054  opabresid  6060  asymref2  6129  intirr  6130  coi1  6285  cnvso  6315  iotaval2  6535  brprcneu  6906  brprcneuALT  6907  dffv2  7011  fvn0ssdmfun  7106  f1oiso  7390  fvmpopr2d  7614  fsplit  8165  poxp2  8197  poxp3  8204  qsid  8840  mapsnend  9102  marypha2lem2  9465  fiinfg  9530  dfac5lem2  10242  dfac5lem3  10243  kmlem15  10282  brdom7disj  10649  suplem2pr  11177  wloglei  11888  fimaxre  12301  arch  12643  dflt2  13317  hashgt12el  14608  hashge2el2dif  14666  summo  15927  tosso  18641  opsrtoslem1  22419  mamulid  22811  mpomatmul  22816  mattpos1  22826  scmatscm  22883  1marepvmarrepid  22945  matunitlindflem2  23050  ist1-3  23722  unisngl  23901  fmid  24334  tgphaus  24491  dscopn  24947  iundisj2  25925  dvlip  26368  ply1divmo  26509  addsrid  28407  mulsrid  28556  disjabrex  33274  disjabrexf  33275  iundisj2f  33282  iundisj2fi  33485  grplsm0l  34058  esplyfvaln  34317  ordtconnlem1  34667  dfdm5  36752  dfrn5  36753  dffun10  36891  elfuns  36892  dfiota3  36900  brimg  36914  dfrdg4  36930  nn0prpwlem  37325  coi1res  38199  bj-axseprep  38260  fvineqsneu  38602  wl-equsalcom  38743  wl-sb9v  38749  ref5  39517  dfsucmap3  39661  pmapglb  41093  polval2N  41229  diclspsn  42517  sn-iotalem  43542  eq0rabdioph  44053  ontric3g  44784  undmrnresiss  44865  relopabVD  46143  icheq  48817  ichexmpl1  48824  pgnbgreunbgrlem4  49490  itsclquadeu  50220  oppcendc  50463