Definition df-stab 839

Description: Propositions where a double-negative can be removed are called stable. See Chapter 2 [Moschovakis] p. 2.

Our notation for stability is a connective STAB which we place before the formula in question. For example, STAB 𝑥 = 𝑦 corresponds to "𝑥 = 𝑦 is stable".

(Contributed by David A. Wheeler, 13-Aug-2018.)

Assertion

Ref	Expression
df-stab	⊢ (STAB 𝜑 ↔ (¬ ¬ 𝜑 → 𝜑))

Detailed syntax breakdown of Definition df-stab

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2	1	wstab 838	. 2 wff STAB 𝜑
3	1	wn 3	. . . 4 wff ¬ 𝜑
4	3	wn 3	. . 3 wff ¬ ¬ 𝜑
5	4, 1	wi 4	. 2 wff (¬ ¬ 𝜑 → 𝜑)
6	2, 5	wb 105	1 wff (STAB 𝜑 ↔ (¬ ¬ 𝜑 → 𝜑))

This definition is referenced by:  stbid  840  stabnot  841  dcstab  852  stdcndc  853  stdcndcOLD  854  stdcn  855  const  860  imanst  896  ddifstab  3355  exmid1stab  4326  fvdifsuppst  6457  suppssrst  6474  suppssrgst  6475  2omotap  7589  bj-trst  16651  bj-fast  16653  bj-nnbist  16656  bj-stim  16658  bj-stan  16659  bj-stand  16660  bj-stal  16661  bj-pm2.18st  16662  bj-con1st  16663  bdstab  16737  subctctexmid  16914  exmidnotnotr  16919