Theorem dcne 2413

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

Assertion

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

Proof of Theorem dcne

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

Syntax hints:  ¬ wn 3   ↔ wb 105   ∨ wo 715  DECID wdc 841   = wceq 1397   ≠ wne 2402

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 716

This theorem depends on definitions:  df-bi 117  df-dc 842  df-ne 2403

This theorem is referenced by:  updjudhf  7277  pr1or2  7398  zdceq  9554  nn0lt2  9560  xlesubadd  10117  qdceq  10503  ccat1st1st  11217  swrdccatin1  11305  xrmaxadd  11821  fsumdvds  12402  nn0seqcvgd  12612  pcxnn0cl  12882  pcxqcl  12884  pcge0  12885  pcdvdsb  12892  pcneg  12897  pcdvdstr  12899  pcgcd1  12900  pc2dvds  12902  pcz  12904  pcprmpw2  12905  pcaddlem  12911  pcadd  12912  pcmpt  12915  qexpz  12924  4sqlem19  12981  lgsneg1  15753  lgsdirprm  15762  lgsdir  15763  lgsne0  15766  lgsdirnn0  15775  lgsdinn0  15776  2sqlem9  15852  upgr1een  15974  usgr1e  16091  tridceq  16660