![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > dcne | GIF version |
Description: Decidable equality expressed in terms of ≠. Basically the same as df-dc 836. (Contributed by Jim Kingdon, 14-Mar-2020.) |
Ref | Expression |
---|---|
dcne | ⊢ (DECID 𝐴 = 𝐵 ↔ (𝐴 = 𝐵 ∨ 𝐴 ≠ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-dc 836 | . 2 ⊢ (DECID 𝐴 = 𝐵 ↔ (𝐴 = 𝐵 ∨ ¬ 𝐴 = 𝐵)) | |
2 | df-ne 2361 | . . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
3 | 2 | orbi2i 763 | . 2 ⊢ ((𝐴 = 𝐵 ∨ 𝐴 ≠ 𝐵) ↔ (𝐴 = 𝐵 ∨ ¬ 𝐴 = 𝐵)) |
4 | 1, 3 | bitr4i 187 | 1 ⊢ (DECID 𝐴 = 𝐵 ↔ (𝐴 = 𝐵 ∨ 𝐴 ≠ 𝐵)) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 ↔ wb 105 ∨ wo 709 DECID wdc 835 = wceq 1364 ≠ wne 2360 |
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 2361 |
This theorem is referenced by: updjudhf 7109 zdceq 9359 nn0lt2 9365 xlesubadd 9915 qdceq 10279 xrmaxadd 11304 nn0seqcvgd 12076 pcxnn0cl 12345 pcxqcl 12347 pcge0 12348 pcdvdsb 12355 pcneg 12360 pcdvdstr 12362 pcgcd1 12363 pc2dvds 12365 pcz 12367 pcprmpw2 12368 pcaddlem 12374 pcadd 12375 pcmpt 12378 qexpz 12387 4sqlem19 12444 lgsneg1 14904 lgsdirprm 14913 lgsdir 14914 lgsne0 14917 lgsdirnn0 14926 lgsdinn0 14927 2sqlem9 14949 tridceq 15283 |
Copyright terms: Public domain | W3C validator |