Theorem dcne 2351

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

Assertion

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

Proof of Theorem dcne

Step	Hyp	Ref	Expression
1		df-dc 830	. 2 ⊢ (DECID 𝐴 = 𝐵 ↔ (𝐴 = 𝐵 ∨ ¬ 𝐴 = 𝐵))
2		df-ne 2341	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	2	orbi2i 757	. 2 ⊢ ((𝐴 = 𝐵 ∨ 𝐴 ≠ 𝐵) ↔ (𝐴 = 𝐵 ∨ ¬ 𝐴 = 𝐵))
4	1, 3	bitr4i 186	1 ⊢ (DECID 𝐴 = 𝐵 ↔ (𝐴 = 𝐵 ∨ 𝐴 ≠ 𝐵))

Syntax hints:  ¬ wn 3   ↔ wb 104   ∨ wo 703  DECID wdc 829   = wceq 1348   ≠ wne 2340

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704

This theorem depends on definitions:  df-bi 116  df-dc 830  df-ne 2341

This theorem is referenced by:  updjudhf  7056  zdceq  9287  nn0lt2  9293  xlesubadd  9840  qdceq  10203  xrmaxadd  11224  nn0seqcvgd  11995  pcxnn0cl  12264  pcge0  12266  pcdvdsb  12273  pcneg  12278  pcdvdstr  12280  pcgcd1  12281  pc2dvds  12283  pcz  12285  pcprmpw2  12286  pcaddlem  12292  pcadd  12293  pcmpt  12295  qexpz  12304  lgsneg1  13720  lgsdirprm  13729  lgsdir  13730  lgsne0  13733  lgsdirnn0  13742  lgsdinn0  13743  2sqlem9  13754  tridceq  14088