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 = { 𝑥 ∣ ( ∃ 𝑧 ∈ PROP ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ PROP 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) }

Proof

Step	Hyp	Ref	Expression
1		dfprop2	⊢ PROP ⊆ { 𝑥 ∣ ( ∃ 𝑧 ∈ PROP ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ PROP 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) }
2		dfprop1	⊢ { 𝑥 ∣ ( ∃ 𝑧 ∈ PROP ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ PROP 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } ⊆ PROP
3	1 2	eqssi	⊢ PROP = { 𝑥 ∣ ( ∃ 𝑧 ∈ PROP ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ PROP 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) }