Theorem dcne 2389

Description: Decidable equality expressed in terms of =/=. Basically the same as df-dc 837. (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 837	. 2 |- (DECID A = B <-> ( A = B \/ -. A = B ) )
2		df-ne 2379	. . 3 |- ( A =/= B <-> -. A = B )
3	2	orbi2i 764	. 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 710  DECID wdc 836   = wceq 1373   =/= wne 2378

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 711

This theorem depends on definitions:  df-bi 117  df-dc 837  df-ne 2379

This theorem is referenced by:  updjudhf  7207  pr1or2  7328  zdceq  9483  nn0lt2  9489  xlesubadd  10040  qdceq  10424  ccat1st1st  11131  swrdccatin1  11216  xrmaxadd  11687  fsumdvds  12268  nn0seqcvgd  12478  pcxnn0cl  12748  pcxqcl  12750  pcge0  12751  pcdvdsb  12758  pcneg  12763  pcdvdstr  12765  pcgcd1  12766  pc2dvds  12768  pcz  12770  pcprmpw2  12771  pcaddlem  12777  pcadd  12778  pcmpt  12781  qexpz  12790  4sqlem19  12847  lgsneg1  15617  lgsdirprm  15626  lgsdir  15627  lgsne0  15630  lgsdirnn0  15639  lgsdinn0  15640  2sqlem9  15716  tridceq  16197