Metamath Proof Explorer

Theorem dfprop2

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

Ref Expression
Assertion dfprop2 Could not format assertion : 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 |-

Proof

Step Hyp Ref Expression
1 df-prop 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 |- 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 |-
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 sstr2 Could not format ( a C_ { x | ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } -> ( { 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 -> a C_ PROP ) ) : No typesetting found for |- ( a C_ { x | ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } -> ( { 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 -> a C_ PROP ) ) with typecode |-
4 2 3 mpi Could not format ( a C_ { x | ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } -> a C_ PROP ) : No typesetting found for |- ( a C_ { x | ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } -> a C_ PROP ) with typecode |-
5 rexeq Could not format ( y = a -> ( E. w e. y x = ( w prop-> z ) <-> E. w e. a x = ( w prop-> z ) ) ) : No typesetting found for |- ( y = a -> ( E. w e. y x = ( w prop-> z ) <-> E. w e. a x = ( w prop-> z ) ) ) with typecode |-
6 5 orbi2d Could not format ( y = a -> ( ( x = ( prop-. ` z ) \/ E. w e. y x = ( w prop-> z ) ) <-> ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) ) ) : No typesetting found for |- ( y = a -> ( ( x = ( prop-. ` z ) \/ E. w e. y x = ( w prop-> z ) ) <-> ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) ) ) with typecode |-
7 6 rexeqbi1dv Could not format ( y = a -> ( E. z e. y ( x = ( prop-. ` z ) \/ E. w e. y x = ( w prop-> z ) ) <-> E. z e. a ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) ) ) : No typesetting found for |- ( y = a -> ( E. z e. y ( x = ( prop-. ` z ) \/ E. w e. y x = ( w prop-> z ) ) <-> E. z e. a ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) ) ) with typecode |-
8 7 orbi1d Could not format ( y = a -> ( ( E. z e. y ( x = ( prop-. ` z ) \/ E. w e. y x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) <-> ( E. z e. a ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) ) ) : No typesetting found for |- ( y = a -> ( ( E. z e. y ( x = ( prop-. ` z ) \/ E. w e. y x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) <-> ( E. z e. a ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) ) ) with typecode |-
9 8 abbidv Could not format ( y = a -> { x | ( E. z e. y ( x = ( prop-. ` z ) \/ E. w e. y x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } = { x | ( E. z e. a ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } ) : No typesetting found for |- ( y = a -> { x | ( E. z e. y ( x = ( prop-. ` z ) \/ E. w e. y x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } = { x | ( E. z e. a ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } ) with typecode |-
10 eqid 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 ) ) } ) = ( 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 |- ( 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 ) ) } ) = ( 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 |-
11 vex ⊢ a ∈ V
12 11 dfproplem Could not format { x | ( E. z e. a ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } e. _V : No typesetting found for |- { x | ( E. z e. a ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } e. _V with typecode |-
13 9 10 12 fvmpt Could not format ( a e. _V -> ( ( 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 ) ) } ) ` a ) = { x | ( E. z e. a ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } ) : No typesetting found for |- ( a e. _V -> ( ( 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 ) ) } ) ` a ) = { x | ( E. z e. a ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } ) with typecode |-
14 13 elv 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 ) ) } ) ` a ) = { x | ( E. z e. a ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } : No typesetting found for |- ( ( 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 ) ) } ) ` a ) = { x | ( E. z e. a ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } with typecode |-
15 ssrexv Could not format ( a C_ PROP -> ( E. z e. a ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) -> E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) ) ) : No typesetting found for |- ( a C_ PROP -> ( E. z e. a ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) -> E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) ) ) with typecode |-
16 15 orim1d Could not format ( a C_ PROP -> ( ( E. z e. a ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) -> ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) ) ) : No typesetting found for |- ( a C_ PROP -> ( ( E. z e. a ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) -> ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) ) ) with typecode |-
17 ssrexv Could not format ( a C_ PROP -> ( E. w e. a x = ( w prop-> z ) -> E. w e. PROP x = ( w prop-> z ) ) ) : No typesetting found for |- ( a C_ PROP -> ( E. w e. a x = ( w prop-> z ) -> E. w e. PROP x = ( w prop-> z ) ) ) with typecode |-
18 17 orim2d Could not format ( a C_ PROP -> ( ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) -> ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) ) ) : No typesetting found for |- ( a C_ PROP -> ( ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) -> ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) ) ) with typecode |-
19 18 reximdv Could not format ( a C_ PROP -> ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) -> E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) ) ) : No typesetting found for |- ( a C_ PROP -> ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) -> E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) ) ) with typecode |-
20 19 orim1d Could not format ( a C_ PROP -> ( ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) -> ( 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 |- ( a C_ PROP -> ( ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) -> ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) ) ) with typecode |-
21 16 20 syld Could not format ( a C_ PROP -> ( ( E. z e. a ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) -> ( 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 |- ( a C_ PROP -> ( ( E. z e. a ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) -> ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) ) ) with typecode |-
22 21 ss2abdv Could not format ( a C_ PROP -> { x | ( E. z e. a ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } 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 |- ( a C_ PROP -> { x | ( E. z e. a ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } 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 |-
23 14 22 eqsstrid Could not format ( a C_ PROP -> ( ( 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 ) ) } ) ` a ) 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 |- ( a C_ PROP -> ( ( 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 ) ) } ) ` a ) 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 |-
24 4 23 syl Could not format ( a C_ { x | ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } -> ( ( 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 ) ) } ) ` a ) 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 |- ( a C_ { x | ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } -> ( ( 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 ) ) } ) ` a ) 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 |-
25 24 ax-gen Could not format A. a ( a C_ { x | ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } -> ( ( 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 ) ) } ) ` a ) 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 |- A. a ( a C_ { x | ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } -> ( ( 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 ) ) } ) ` a ) 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 |-
26 25 a1i Could not format ( T. -> A. a ( a C_ { x | ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } -> ( ( 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 ) ) } ) ` a ) 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 |- ( T. -> A. a ( a C_ { x | ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } -> ( ( 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 ) ) } ) ` a ) 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 |-
27 1 26 setrec2v Could not format ( T. -> 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 |- ( T. -> 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 |-
28 27 mptru 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 |-