Theorem dcne 2358

Description: Decidable equality expressed in terms of ≠. Basically the same as df-dc 835. (Contributed by Jim Kingdon, 14-Mar-2020.)

Assertion

Ref	Expression
dcne	⊢ (DECID 𝐴 = 𝐵 ↔ (𝐴 = 𝐵 ∨ 𝐴 ≠ 𝐵))

Proof of Theorem dcne

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

Syntax hints:  ¬ wn 3   ↔ wb 105   ∨ wo 708  DECID wdc 834   = wceq 1353   ≠ wne 2347

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 709

This theorem depends on definitions:  df-bi 117  df-dc 835  df-ne 2348

This theorem is referenced by:  updjudhf  7078  zdceq  9328  nn0lt2  9334  xlesubadd  9883  qdceq  10247  xrmaxadd  11269  nn0seqcvgd  12041  pcxnn0cl  12310  pcge0  12312  pcdvdsb  12319  pcneg  12324  pcdvdstr  12326  pcgcd1  12327  pc2dvds  12329  pcz  12331  pcprmpw2  12332  pcaddlem  12338  pcadd  12339  pcmpt  12341  qexpz  12350  lgsneg1  14429  lgsdirprm  14438  lgsdir  14439  lgsne0  14442  lgsdirnn0  14451  lgsdinn0  14452  2sqlem9  14474  tridceq  14807