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  7420  pr1or2  7541  zdceq  9725  nn0lt2  9732  xlesubadd  10296  qdceq  10690  ccat1st1st  11425  swrdccatin1  11513  xrmaxadd  12046  fsumdvds  12628  nn0seqcvgd  12838  pcxnn0cl  13112  pcxqcl  13114  pcge0  13115  pcdvdsb  13122  pcneg  13127  pcdvdstr  13129  pcgcd1  13130  pc2dvds  13132  pcz  13134  pcprmpw2  13135  pcaddlem  13141  pcadd  13142  pcmpt  13145  qexpz  13154  4sqlem19  13211  prmlem1a  13244  lgsneg1  16310  lgsdirprm  16319  lgsdir  16320  lgsne0  16323  lgsdirnn0  16332  lgsdinn0  16333  2sqlem9  16409  upgr1een  16531  usgr1e  16648  eupth2lem3lem3fi  16877  eupth2lem3lem7fi  16881  tridceq  17273