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  7183  zdceq  9450  nn0lt2  9456  xlesubadd  10007  qdceq  10389  ccat1st1st  11096  xrmaxadd  11605  fsumdvds  12186  nn0seqcvgd  12396  pcxnn0cl  12666  pcxqcl  12668  pcge0  12669  pcdvdsb  12676  pcneg  12681  pcdvdstr  12683  pcgcd1  12684  pc2dvds  12686  pcz  12688  pcprmpw2  12689  pcaddlem  12695  pcadd  12696  pcmpt  12699  qexpz  12708  4sqlem19  12765  lgsneg1  15535  lgsdirprm  15544  lgsdir  15545  lgsne0  15548  lgsdirnn0  15557  lgsdinn0  15558  2sqlem9  15634  tridceq  16032