Theorem dcne 2386

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

Assertion

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

Proof of Theorem dcne

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

Syntax hints:  ¬ wn 3   ↔ wb 105   ∨ wo 709  DECID wdc 835   = wceq 1372   ≠ wne 2375

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 710

This theorem depends on definitions:  df-bi 117  df-dc 836  df-ne 2376

This theorem is referenced by:  updjudhf  7180  zdceq  9447  nn0lt2  9453  xlesubadd  10004  qdceq  10385  xrmaxadd  11514  fsumdvds  12095  nn0seqcvgd  12305  pcxnn0cl  12575  pcxqcl  12577  pcge0  12578  pcdvdsb  12585  pcneg  12590  pcdvdstr  12592  pcgcd1  12593  pc2dvds  12595  pcz  12597  pcprmpw2  12598  pcaddlem  12604  pcadd  12605  pcmpt  12608  qexpz  12617  4sqlem19  12674  lgsneg1  15444  lgsdirprm  15453  lgsdir  15454  lgsne0  15457  lgsdirnn0  15466  lgsdinn0  15467  2sqlem9  15543  tridceq  15928