Theorem dcne 2413

Description: Decidable equality expressed in terms of =/=. Basically the same as df-dc 842. (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 842	. 2 |- (DECID A = B <-> ( A = B \/ -. A = B ) )
2		df-ne 2403	. . 3 |- ( A =/= B <-> -. A = B )
3	2	orbi2i 769	. 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 715  DECID wdc 841   = wceq 1397   =/= wne 2402

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 716

This theorem depends on definitions:  df-bi 117  df-dc 842  df-ne 2403

This theorem is referenced by:  updjudhf  7278  pr1or2  7399  zdceq  9555  nn0lt2  9561  xlesubadd  10118  qdceq  10505  ccat1st1st  11222  swrdccatin1  11310  xrmaxadd  11839  fsumdvds  12421  nn0seqcvgd  12631  pcxnn0cl  12901  pcxqcl  12903  pcge0  12904  pcdvdsb  12911  pcneg  12916  pcdvdstr  12918  pcgcd1  12919  pc2dvds  12921  pcz  12923  pcprmpw2  12924  pcaddlem  12930  pcadd  12931  pcmpt  12934  qexpz  12943  4sqlem19  13000  lgsneg1  15773  lgsdirprm  15782  lgsdir  15783  lgsne0  15786  lgsdirnn0  15795  lgsdinn0  15796  2sqlem9  15872  upgr1een  15994  usgr1e  16111  eupth2lem3lem3fi  16340  eupth2lem3lem7fi  16344  tridceq  16712