Theorem dfprop

Description: The set of sentences of propositional calculus is equal to the set of sentences that are either a variable encoded as a natural number, a negation of a sentence propositional calculus, or an implication between two sentences of propositional calculus. (Contributed by Thomas van Maaren, 21-Aug-2026)

	Ref	Expression
Assertion	dfprop	|- PROP = { x | ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) }

Proof

Step	Hyp	Ref	Expression
1		dfprop2	|- PROP C_ { x | ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) }
2		dfprop1	|- { x | ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } C_ PROP
3	1 2	eqssi	|- PROP = { x | ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) }