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  7246  pr1or2  7367  zdceq  9522  nn0lt2  9528  xlesubadd  10079  qdceq  10464  ccat1st1st  11172  swrdccatin1  11257  xrmaxadd  11772  fsumdvds  12353  nn0seqcvgd  12563  pcxnn0cl  12833  pcxqcl  12835  pcge0  12836  pcdvdsb  12843  pcneg  12848  pcdvdstr  12850  pcgcd1  12851  pc2dvds  12853  pcz  12855  pcprmpw2  12856  pcaddlem  12862  pcadd  12863  pcmpt  12866  qexpz  12875  4sqlem19  12932  lgsneg1  15704  lgsdirprm  15713  lgsdir  15714  lgsne0  15717  lgsdirnn0  15726  lgsdinn0  15727  2sqlem9  15803  tridceq  16424