Theorem dcne 2431

Description: Decidable equality expressed in terms of =/=. Basically the same as df-dc 847. (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 847	. 2 |- (DECID A = B <-> ( A = B \/ -. A = B ) )
2		df-ne 2421	. . 3 |- ( A =/= B <-> -. A = B )
3	2	orbi2i 774	. 2 |- ( ( A = B \/ A =/= B ) <-> ( A = B \/ -. A = B ) )
4	1, 3	bitr4i 187	1 |- (DECID A = B <-> ( A = B \/ A =/= B ) )

This proof depends on syntax axioms:   -. wn 3   <-> wb 105   \/ wo 720  DECID wdc 846   = wceq 1402   =/= wne 2420

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117  df-dc 847  df-ne 2421

This theorem is used by:  updjudhf  7419  pr1or2  7540  zdceq  9720  nn0lt2  9727  xlesubadd  10285  qdceq  10679  ccat1st1st  11409  swrdccatin1  11497  xrmaxadd  12027  fsumdvds  12609  nn0seqcvgd  12819  pcxnn0cl  13089  pcxqcl  13091  pcge0  13092  pcdvdsb  13099  pcneg  13104  pcdvdstr  13106  pcgcd1  13107  pc2dvds  13109  pcz  13111  pcprmpw2  13112  pcaddlem  13118  pcadd  13119  pcmpt  13122  qexpz  13131  4sqlem19  13188  lgsneg1  16144  lgsdirprm  16153  lgsdir  16154  lgsne0  16157  lgsdirnn0  16166  lgsdinn0  16167  2sqlem9  16243  upgr1een  16365  usgr1e  16482  eupth2lem3lem3fi  16711  eupth2lem3lem7fi  16715  tridceq  17106