Definition df-prop 38554

Description: Define the language of propositional calculus. This definition is noncircular. For a more usable and intuitive, but circular, definition see dfprop 38561. (Contributed by Thomas van Maaren, 21-Aug-2026.)

Assertion

Ref	Expression
df-prop	⊢ PROP = setrecs((𝑦 ∈ V ↦ {𝑥 ∣ (∃𝑧 ∈ 𝑦 (𝑥 = (prop¬‘𝑧) ∨ ∃𝑤 ∈ 𝑦 𝑥 = (𝑤prop→𝑧)) ∨ ∃𝑛 ∈ ℕ 𝑥 = (propvar ‘𝑛))}))

Distinct variable group:   𝑤,𝑛,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-prop

Step	Hyp	Ref	Expression
1		cprop 38553	. 2 class PROP
2		vy	. . . 4 setvar 𝑦
3		cvv 3450	. . . 4 class V
4		vx	. . . . . . . . . 10 setvar 𝑥
5	4	cv 1569	. . . . . . . . 9 class 𝑥
6		vz	. . . . . . . . . . 11 setvar 𝑧
7	6	cv 1569	. . . . . . . . . 10 class 𝑧
8		cpropneg 38548	. . . . . . . . . 10 class prop¬
9	7, 8	cfv 6528	. . . . . . . . 9 class (prop¬‘𝑧)
10	5, 9	wceq 1570	. . . . . . . 8 wff 𝑥 = (prop¬‘𝑧)
11		vw	. . . . . . . . . . . 12 setvar 𝑤
12	11	cv 1569	. . . . . . . . . . 11 class 𝑤
13		cpropimp 38549	. . . . . . . . . . 11 class prop→
14	12, 7, 13	co 7409	. . . . . . . . . 10 class (𝑤prop→𝑧)
15	5, 14	wceq 1570	. . . . . . . . 9 wff 𝑥 = (𝑤prop→𝑧)
16	2	cv 1569	. . . . . . . . 9 class 𝑦
17	15, 11, 16	wrex 3086	. . . . . . . 8 wff ∃𝑤 ∈ 𝑦 𝑥 = (𝑤prop→𝑧)
18	10, 17	wo 861	. . . . . . 7 wff (𝑥 = (prop¬‘𝑧) ∨ ∃𝑤 ∈ 𝑦 𝑥 = (𝑤prop→𝑧))
19	18, 6, 16	wrex 3086	. . . . . 6 wff ∃𝑧 ∈ 𝑦 (𝑥 = (prop¬‘𝑧) ∨ ∃𝑤 ∈ 𝑦 𝑥 = (𝑤prop→𝑧))
20		vn	. . . . . . . . . 10 setvar 𝑛
21	20	cv 1569	. . . . . . . . 9 class 𝑛
22		cpropvar 38547	. . . . . . . . 9 class propvar
23	21, 22	cfv 6528	. . . . . . . 8 class (propvar ‘𝑛)
24	5, 23	wceq 1570	. . . . . . 7 wff 𝑥 = (propvar ‘𝑛)
25		cn 12290	. . . . . . 7 class ℕ
26	24, 20, 25	wrex 3086	. . . . . 6 wff ∃𝑛 ∈ ℕ 𝑥 = (propvar ‘𝑛)
27	19, 26	wo 861	. . . . 5 wff (∃𝑧 ∈ 𝑦 (𝑥 = (prop¬‘𝑧) ∨ ∃𝑤 ∈ 𝑦 𝑥 = (𝑤prop→𝑧)) ∨ ∃𝑛 ∈ ℕ 𝑥 = (propvar ‘𝑛))
28	27, 4	cab 2738	. . . 4 class {𝑥 ∣ (∃𝑧 ∈ 𝑦 (𝑥 = (prop¬‘𝑧) ∨ ∃𝑤 ∈ 𝑦 𝑥 = (𝑤prop→𝑧)) ∨ ∃𝑛 ∈ ℕ 𝑥 = (propvar ‘𝑛))}
29	2, 3, 28	cmpt 5186	. . 3 class (𝑦 ∈ V ↦ {𝑥 ∣ (∃𝑧 ∈ 𝑦 (𝑥 = (prop¬‘𝑧) ∨ ∃𝑤 ∈ 𝑦 𝑥 = (𝑤prop→𝑧)) ∨ ∃𝑛 ∈ ℕ 𝑥 = (propvar ‘𝑛))})
30	29	csetrecs 9921	. 2 class setrecs((𝑦 ∈ V ↦ {𝑥 ∣ (∃𝑧 ∈ 𝑦 (𝑥 = (prop¬‘𝑧) ∨ ∃𝑤 ∈ 𝑦 𝑥 = (𝑤prop→𝑧)) ∨ ∃𝑛 ∈ ℕ 𝑥 = (propvar ‘𝑛))}))
31	1, 30	wceq 1570	1 wff PROP = setrecs((𝑦 ∈ V ↦ {𝑥 ∣ (∃𝑧 ∈ 𝑦 (𝑥 = (prop¬‘𝑧) ∨ ∃𝑤 ∈ 𝑦 𝑥 = (𝑤prop→𝑧)) ∨ ∃𝑛 ∈ ℕ 𝑥 = (propvar ‘𝑛))}))

This definition is used by:  varprop  38556  negprop  38557  impprop  38558  dfprop2  38560