Theorem dcne 2378

Description: Decidable equality expressed in terms of =/=. Basically the same as df-dc 836. (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 836	. 2 |- (DECID A = B <-> ( A = B \/ -. A = B ) )
2		df-ne 2368	. . 3 |- ( A =/= B <-> -. A = B )
3	2	orbi2i 763	. 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 709  DECID wdc 835   = wceq 1364   =/= wne 2367

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 710

This theorem depends on definitions:  df-bi 117  df-dc 836  df-ne 2368

This theorem is referenced by:  updjudhf  7145  zdceq  9401  nn0lt2  9407  xlesubadd  9958  qdceq  10334  xrmaxadd  11426  fsumdvds  12007  nn0seqcvgd  12209  pcxnn0cl  12479  pcxqcl  12481  pcge0  12482  pcdvdsb  12489  pcneg  12494  pcdvdstr  12496  pcgcd1  12497  pc2dvds  12499  pcz  12501  pcprmpw2  12502  pcaddlem  12508  pcadd  12509  pcmpt  12512  qexpz  12521  4sqlem19  12578  lgsneg1  15266  lgsdirprm  15275  lgsdir  15276  lgsne0  15279  lgsdirnn0  15288  lgsdinn0  15289  2sqlem9  15365  tridceq  15700