Definition df-prop

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

	Ref	Expression
Assertion	df-prop	Could not format assertion : No typesetting found for |- PROP = setrecs ( ( y e. _V |-> { x | ( E. z e. y ( x = ( prop-. ` z ) \/ E. w e. y x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cprop	Could not format PROP : No typesetting found for class PROP with typecode class
1		vy	$$setvary$$
2		cvv	$$class\mathrm{V}$$
3		vx	$$setvarx$$
4		vz	$$setvarz$$
5	1	cv	$$setvary$$
6	3	cv	$$setvarx$$
7		cpropneg	Could not format prop-. : No typesetting found for class prop-. with typecode class
8	4	cv	$$setvarz$$
9	8 7	cfv	Could not format ( prop-. ` z ) : No typesetting found for class ( prop-. ` z ) with typecode class
10	6 9	wceq	Could not format x = ( prop-. ` z ) : No typesetting found for wff x = ( prop-. ` z ) with typecode wff
11		vw	$$setvarw$$
12	11	cv	$$setvarw$$
13		cpropimp	Could not format prop-> : No typesetting found for class prop-> with typecode class
14	12 8 13	co	Could not format ( w prop-> z ) : No typesetting found for class ( w prop-> z ) with typecode class
15	6 14	wceq	Could not format x = ( w prop-> z ) : No typesetting found for wff x = ( w prop-> z ) with typecode wff
16	15 11 5	wrex	Could not format E. w e. y x = ( w prop-> z ) : No typesetting found for wff E. w e. y x = ( w prop-> z ) with typecode wff
17	10 16	wo	Could not format ( x = ( prop-. ` z ) \/ E. w e. y x = ( w prop-> z ) ) : No typesetting found for wff ( x = ( prop-. ` z ) \/ E. w e. y x = ( w prop-> z ) ) with typecode wff
18	17 4 5	wrex	Could not format E. z e. y ( x = ( prop-. ` z ) \/ E. w e. y x = ( w prop-> z ) ) : No typesetting found for wff E. z e. y ( x = ( prop-. ` z ) \/ E. w e. y x = ( w prop-> z ) ) with typecode wff
19		vn	$$setvarn$$
20		cn	$$class\mathbb{N}$$
21		cpropvar	Could not format propvar : No typesetting found for class propvar with typecode class
22	19	cv	$$setvarn$$
23	22 21	cfv	Could not format ( propvar ` n ) : No typesetting found for class ( propvar ` n ) with typecode class
24	6 23	wceq	Could not format x = ( propvar ` n ) : No typesetting found for wff x = ( propvar ` n ) with typecode wff
25	24 19 20	wrex	Could not format E. n e. NN x = ( propvar ` n ) : No typesetting found for wff E. n e. NN x = ( propvar ` n ) with typecode wff
26	18 25	wo	Could not format ( E. z e. y ( x = ( prop-. ` z ) \/ E. w e. y x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) : No typesetting found for wff ( E. z e. y ( x = ( prop-. ` z ) \/ E. w e. y x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) with typecode wff
27	26 3	cab	Could not format { x | ( E. z e. y ( x = ( prop-. ` z ) \/ E. w e. y x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } : No typesetting found for class { x | ( E. z e. y ( x = ( prop-. ` z ) \/ E. w e. y x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } with typecode class
28	1 2 27	cmpt	Could not format ( y e. _V |-> { x | ( E. z e. y ( x = ( prop-. ` z ) \/ E. w e. y x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } ) : No typesetting found for class ( y e. _V |-> { x | ( E. z e. y ( x = ( prop-. ` z ) \/ E. w e. y x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } ) with typecode class
29	28	csetrecs	Could not format setrecs ( ( y e. _V |-> { x | ( E. z e. y ( x = ( prop-. ` z ) \/ E. w e. y x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } ) ) : No typesetting found for class setrecs ( ( y e. _V |-> { x | ( E. z e. y ( x = ( prop-. ` z ) \/ E. w e. y x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } ) ) with typecode class
30	0 29	wceq	Could not format PROP = setrecs ( ( y e. _V |-> { x | ( E. z e. y ( x = ( prop-. ` z ) \/ E. w e. y x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } ) ) : No typesetting found for wff PROP = setrecs ( ( y e. _V |-> { x | ( E. z e. y ( x = ( prop-. ` z ) \/ E. w e. y x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } ) ) with typecode wff