Theorem dcne 2414

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

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 717

This theorem depends on definitions:  df-bi 117  df-dc 843  df-ne 2404

This theorem is referenced by:  updjudhf  7338  pr1or2  7459  zdceq  9616  nn0lt2  9622  xlesubadd  10179  qdceq  10567  ccat1st1st  11284  swrdccatin1  11372  xrmaxadd  11901  fsumdvds  12483  nn0seqcvgd  12693  pcxnn0cl  12963  pcxqcl  12965  pcge0  12966  pcdvdsb  12973  pcneg  12978  pcdvdstr  12980  pcgcd1  12981  pc2dvds  12983  pcz  12985  pcprmpw2  12986  pcaddlem  12992  pcadd  12993  pcmpt  12996  qexpz  13005  4sqlem19  13062  lgsneg1  15844  lgsdirprm  15853  lgsdir  15854  lgsne0  15857  lgsdirnn0  15866  lgsdinn0  15867  2sqlem9  15943  upgr1een  16065  usgr1e  16182  eupth2lem3lem3fi  16411  eupth2lem3lem7fi  16415  tridceq  16789