Definition df-wexmid 17041

Description: Weak excluded middle is the principle that any negated proposition is decidable. (Contributed by Jim Kingdon, 30-Jul-2026.)

Assertion

Ref	Expression
df-wexmid	⊢ (WEXMID ↔ ∀𝑝 ∈ 𝒫 1o(¬ 𝑝 = 1o ∨ ¬ ¬ 𝑝 = 1o))

Detailed syntax breakdown of Definition df-wexmid

Step	Hyp	Ref	Expression
1		wwem 17040	. 2 wff WEXMID
2		vp	. . . . . . 7 setvar 𝑝
3	2	cv 1401	. . . . . 6 class 𝑝
4		c1o 6680	. . . . . 6 class 1o
5	3, 4	wceq 1402	. . . . 5 wff 𝑝 = 1o
6	5	wn 3	. . . 4 wff ¬ 𝑝 = 1o
7	6	wn 3	. . . 4 wff ¬ ¬ 𝑝 = 1o
8	6, 7	wo 720	. . 3 wff (¬ 𝑝 = 1o ∨ ¬ ¬ 𝑝 = 1o)
9	4	cpw 3688	. . 3 class 𝒫 1o
10	8, 2, 9	wral 2528	. 2 wff ∀𝑝 ∈ 𝒫 1o(¬ 𝑝 = 1o ∨ ¬ ¬ 𝑝 = 1o)
11	1, 10	wb 105	1 wff (WEXMID ↔ ∀𝑝 ∈ 𝒫 1o(¬ 𝑝 = 1o ∨ ¬ ¬ 𝑝 = 1o))

This definition is used by:  wexmiddc  17042  wexmiddiffi  17044  wexmiddifxy  17046