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	Could not format assertion : No typesetting found for |- PROP = { x | ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } with typecode |-

Proof

Step	Hyp	Ref	Expression
1		dfprop2	Could not format 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 ) ) } : No typesetting found for |- 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 ) ) } with typecode |-
2		dfprop1	Could not format { 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 : No typesetting found for |- { 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 with typecode |-
3	1 2	eqssi	Could not format PROP = { x | ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } : No typesetting found for |- PROP = { x | ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } with typecode |-