Theorem dcne 2387

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 2377	. . 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 2376

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 2377

This theorem is referenced by:  updjudhf  7181  zdceq  9448  nn0lt2  9454  xlesubadd  10005  qdceq  10387  ccat1st1st  11093  xrmaxadd  11572  fsumdvds  12153  nn0seqcvgd  12363  pcxnn0cl  12633  pcxqcl  12635  pcge0  12636  pcdvdsb  12643  pcneg  12648  pcdvdstr  12650  pcgcd1  12651  pc2dvds  12653  pcz  12655  pcprmpw2  12656  pcaddlem  12662  pcadd  12663  pcmpt  12666  qexpz  12675  4sqlem19  12732  lgsneg1  15502  lgsdirprm  15511  lgsdir  15512  lgsne0  15515  lgsdirnn0  15524  lgsdinn0  15525  2sqlem9  15601  tridceq  15995