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 𝐴 = 𝐵 ↔ (𝐴 = 𝐵 ∨ 𝐴 ≠ 𝐵))

Proof of Theorem dcne

Step	Hyp	Ref	Expression
1		df-dc 847	. 2 ⊢ (DECID 𝐴 = 𝐵 ↔ (𝐴 = 𝐵 ∨ ¬ 𝐴 = 𝐵))
2		df-ne 2421	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	2	orbi2i 774	. 2 ⊢ ((𝐴 = 𝐵 ∨ 𝐴 ≠ 𝐵) ↔ (𝐴 = 𝐵 ∨ ¬ 𝐴 = 𝐵))
4	1, 3	bitr4i 187	1 ⊢ (DECID 𝐴 = 𝐵 ↔ (𝐴 = 𝐵 ∨ 𝐴 ≠ 𝐵))

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  7425  pr1or2  7546  zdceq  9731  nn0lt2  9738  xlesubadd  10302  qdceq  10696  ccat1st1st  11431  swrdccatin1  11519  xrmaxadd  12052  fsumdvds  12634  nn0seqcvgd  12844  pcxnn0cl  13118  pcxqcl  13120  pcge0  13121  pcdvdsb  13128  pcneg  13133  pcdvdstr  13135  pcgcd1  13136  pc2dvds  13138  pcz  13140  pcprmpw2  13141  pcaddlem  13147  pcadd  13148  pcmpt  13151  qexpz  13160  4sqlem19  13217  prmlem1a  13250  lgsneg1  16349  lgsdirprm  16358  lgsdir  16359  lgsne0  16362  lgsdirnn0  16371  lgsdinn0  16372  2sqlem9  16448  upgr1een  16570  usgr1e  16687  eupth2lem3lem3fi  16916  eupth2lem3lem7fi  16920  tridceq  17313