df-wexmid - Mathbox for Jim Kingdon

	Mathbox for Jim Kingdon		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > Mathboxes > df-wexmid		Unicode version

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 $\/$

**Detailed syntax breakdown of Definition df-wexmid**
Step	Hyp	Ref	Expression
1		wwem 17040	. 2 WEXMID
2		vp	. . . . . . 7
3	2	cv 1401	. . . . . 6
4		c1o 6680	. . . . . 6
5	3, 4	wceq 1402	. . . . 5
6	5	wn 3	. . . 4
7	6	wn 3	. . . 4
8	6, 7	wo 720	. . 3 $\/$
9	4	cpw 3688	. . 3
10	8, 2, 9	wral 2528	. 2 $\/$
11	1, 10	wb 105	1 WEXMID $\/$

Colors of variables: wff set class

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