Theorem dcne 2411

Description: Decidable equality expressed in terms of =/=. Basically the same as df-dc 840. (Contributed by Jim Kingdon, 14-Mar-2020.)

Assertion

Ref	Expression
dcne	|- (DECID A = B <-> ( A = B \/ A =/= B ) )

Proof of Theorem dcne

Step	Hyp	Ref	Expression
1		df-dc 840	. 2 |- (DECID A = B <-> ( A = B \/ -. A = B ) )
2		df-ne 2401	. . 3 |- ( A =/= B <-> -. A = B )
3	2	orbi2i 767	. 2 |- ( ( A = B \/ A =/= B ) <-> ( A = B \/ -. A = B ) )
4	1, 3	bitr4i 187	1 |- (DECID A = B <-> ( A = B \/ A =/= B ) )

Syntax hints:   -. wn 3   <-> wb 105   \/ wo 713  DECID wdc 839   = wceq 1395   =/= wne 2400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714

This theorem depends on definitions:  df-bi 117  df-dc 840  df-ne 2401

This theorem is referenced by:  updjudhf  7257  pr1or2  7378  zdceq  9533  nn0lt2  9539  xlesubadd  10091  qdceq  10476  ccat1st1st  11188  swrdccatin1  11273  xrmaxadd  11788  fsumdvds  12369  nn0seqcvgd  12579  pcxnn0cl  12849  pcxqcl  12851  pcge0  12852  pcdvdsb  12859  pcneg  12864  pcdvdstr  12866  pcgcd1  12867  pc2dvds  12869  pcz  12871  pcprmpw2  12872  pcaddlem  12878  pcadd  12879  pcmpt  12882  qexpz  12891  4sqlem19  12948  lgsneg1  15720  lgsdirprm  15729  lgsdir  15730  lgsne0  15733  lgsdirnn0  15742  lgsdinn0  15743  2sqlem9  15819  tridceq  16512