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 A = B <-> ( A = B \/ A =/= B ) )

Proof of Theorem dcne

Step	Hyp	Ref	Expression
1		df-dc 847	. 2 |- (DECID A = B <-> ( A = B \/ -. A = B ) )
2		df-ne 2421	. . 3 |- ( A =/= B <-> -. A = B )
3	2	orbi2i 774	. 2 |- ( ( A = B \/ A =/= B ) <-> ( A = B \/ -. A = B ) )
4	1, 3	bitr4i 187	1 |- (DECID A = B <-> ( A = B \/ A =/= B ) )

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  16242  lgsdirprm  16251  lgsdir  16252  lgsne0  16255  lgsdirnn0  16264  lgsdinn0  16265  2sqlem9  16341  upgr1een  16463  usgr1e  16580  eupth2lem3lem3fi  16809  eupth2lem3lem7fi  16813  tridceq  17204