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  7419  pr1or2  7540  zdceq  9724  nn0lt2  9731  xlesubadd  10295  qdceq  10689  ccat1st1st  11423  swrdccatin1  11511  xrmaxadd  12043  fsumdvds  12625  nn0seqcvgd  12835  pcxnn0cl  13109  pcxqcl  13111  pcge0  13112  pcdvdsb  13119  pcneg  13124  pcdvdstr  13126  pcgcd1  13127  pc2dvds  13129  pcz  13131  pcprmpw2  13132  pcaddlem  13138  pcadd  13139  pcmpt  13142  qexpz  13151  4sqlem19  13208  prmlem1a  13241  lgsneg1  16263  lgsdirprm  16272  lgsdir  16273  lgsne0  16276  lgsdirnn0  16285  lgsdinn0  16286  2sqlem9  16362  upgr1een  16484  usgr1e  16601  eupth2lem3lem3fi  16830  eupth2lem3lem7fi  16834  tridceq  17225