Metamath Proof Explorer

Theorem varprop

Description: Variables encoded as natural numbers are sentences of propositional calculus. (Contributed by Thomas van Maaren, 21-Aug-2026)

Ref Expression
Assertion varprop Could not format assertion : No typesetting found for |- ( n e. NN -> ( propvar ` n ) e. PROP ) 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 0ex ⊢ ∅ ∈ V
3 2 a1i ⊢ n ∈ ℕ → ∅ ∈ V
4 0ss Could not format (/) C_ PROP : No typesetting found for |- (/) C_ PROP with typecode |-
5 4 a1i Could not format ( n e. NN -> (/) C_ PROP ) : No typesetting found for |- ( n e. NN -> (/) C_ PROP ) with typecode |-
6 1 3 5 setrec1 Could not format ( n e. NN -> ( ( 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 ) ) } ) ` (/) ) C_ PROP ) : No typesetting found for |- ( n e. NN -> ( ( 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 ) ) } ) ` (/) ) C_ PROP ) with typecode |-
7 rspe Could not format ( ( n e. NN /\ x = ( propvar ` n ) ) -> E. n e. NN x = ( propvar ` n ) ) : No typesetting found for |- ( ( n e. NN /\ x = ( propvar ` n ) ) -> E. n e. NN x = ( propvar ` n ) ) with typecode |-
8 7 olcd Could not format ( ( n e. NN /\ x = ( propvar ` n ) ) -> ( E. z e. (/) ( x = ( prop-. ` z ) \/ E. w e. (/) x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) ) : No typesetting found for |- ( ( n e. NN /\ x = ( propvar ` n ) ) -> ( E. z e. (/) ( x = ( prop-. ` z ) \/ E. w e. (/) x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) ) with typecode |-
9 8 ex Could not format ( n e. NN -> ( x = ( propvar ` n ) -> ( E. z e. (/) ( x = ( prop-. ` z ) \/ E. w e. (/) x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) ) ) : No typesetting found for |- ( n e. NN -> ( x = ( propvar ` n ) -> ( E. z e. (/) ( x = ( prop-. ` z ) \/ E. w e. (/) x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) ) ) with typecode |-
10 9 alrimiv Could not format ( n e. NN -> A. x ( x = ( propvar ` n ) -> ( E. z e. (/) ( x = ( prop-. ` z ) \/ E. w e. (/) x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) ) ) : No typesetting found for |- ( n e. NN -> A. x ( x = ( propvar ` n ) -> ( E. z e. (/) ( x = ( prop-. ` z ) \/ E. w e. (/) x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) ) ) with typecode |-
11 fvex Could not format ( propvar ` n ) e. _V : No typesetting found for |- ( propvar ` n ) e. _V with typecode |-
12 elab6g Could not format ( ( propvar ` n ) e. _V -> ( ( propvar ` n ) e. { x | ( E. z e. (/) ( x = ( prop-. ` z ) \/ E. w e. (/) x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } <-> A. x ( x = ( propvar ` n ) -> ( E. z e. (/) ( x = ( prop-. ` z ) \/ E. w e. (/) x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) ) ) ) : No typesetting found for |- ( ( propvar ` n ) e. _V -> ( ( propvar ` n ) e. { x | ( E. z e. (/) ( x = ( prop-. ` z ) \/ E. w e. (/) x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } <-> A. x ( x = ( propvar ` n ) -> ( E. z e. (/) ( x = ( prop-. ` z ) \/ E. w e. (/) x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) ) ) ) with typecode |-
13 11 12 ax-mp Could not format ( ( propvar ` n ) e. { x | ( E. z e. (/) ( x = ( prop-. ` z ) \/ E. w e. (/) x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } <-> A. x ( x = ( propvar ` n ) -> ( E. z e. (/) ( x = ( prop-. ` z ) \/ E. w e. (/) x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) ) ) : No typesetting found for |- ( ( propvar ` n ) e. { x | ( E. z e. (/) ( x = ( prop-. ` z ) \/ E. w e. (/) x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } <-> A. x ( x = ( propvar ` n ) -> ( E. z e. (/) ( x = ( prop-. ` z ) \/ E. w e. (/) x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) ) ) with typecode |-
14 10 13 sylibr Could not format ( n e. NN -> ( propvar ` n ) e. { x | ( E. z e. (/) ( x = ( prop-. ` z ) \/ E. w e. (/) x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } ) : No typesetting found for |- ( n e. NN -> ( propvar ` n ) e. { x | ( E. z e. (/) ( x = ( prop-. ` z ) \/ E. w e. (/) x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } ) with typecode |-
15 rexeq Could not format ( y = (/) -> ( E. w e. y x = ( w prop-> z ) <-> E. w e. (/) x = ( w prop-> z ) ) ) : No typesetting found for |- ( y = (/) -> ( E. w e. y x = ( w prop-> z ) <-> E. w e. (/) x = ( w prop-> z ) ) ) with typecode |-
16 15 orbi2d Could not format ( y = (/) -> ( ( x = ( prop-. ` z ) \/ E. w e. y x = ( w prop-> z ) ) <-> ( x = ( prop-. ` z ) \/ E. w e. (/) x = ( w prop-> z ) ) ) ) : No typesetting found for |- ( y = (/) -> ( ( x = ( prop-. ` z ) \/ E. w e. y x = ( w prop-> z ) ) <-> ( x = ( prop-. ` z ) \/ E. w e. (/) x = ( w prop-> z ) ) ) ) with typecode |-
17 16 rexeqbi1dv Could not format ( y = (/) -> ( E. z e. y ( x = ( prop-. ` z ) \/ E. w e. y x = ( w prop-> z ) ) <-> E. z e. (/) ( x = ( prop-. ` z ) \/ E. w e. (/) x = ( w prop-> z ) ) ) ) : No typesetting found for |- ( y = (/) -> ( E. z e. y ( x = ( prop-. ` z ) \/ E. w e. y x = ( w prop-> z ) ) <-> E. z e. (/) ( x = ( prop-. ` z ) \/ E. w e. (/) x = ( w prop-> z ) ) ) ) with typecode |-
18 17 orbi1d Could not format ( y = (/) -> ( ( 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. (/) ( x = ( prop-. ` z ) \/ E. w e. (/) x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) ) ) : No typesetting found for |- ( y = (/) -> ( ( 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. (/) ( x = ( prop-. ` z ) \/ E. w e. (/) x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) ) ) with typecode |-
19 18 abbidv Could not format ( y = (/) -> { 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. (/) ( x = ( prop-. ` z ) \/ E. w e. (/) x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } ) : No typesetting found for |- ( y = (/) -> { 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. (/) ( x = ( prop-. ` z ) \/ E. w e. (/) x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } ) with typecode |-
20 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 |-
21 2 dfproplem Could not format { x | ( E. z e. (/) ( x = ( prop-. ` z ) \/ E. w e. (/) x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } e. _V : No typesetting found for |- { x | ( E. z e. (/) ( x = ( prop-. ` z ) \/ E. w e. (/) x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } e. _V with typecode |-
22 19 20 21 fvmpt Could not format ( (/) 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 ) ) } ) ` (/) ) = { x | ( E. z e. (/) ( x = ( prop-. ` z ) \/ E. w e. (/) x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } ) : No typesetting found for |- ( (/) 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 ) ) } ) ` (/) ) = { x | ( E. z e. (/) ( x = ( prop-. ` z ) \/ E. w e. (/) x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } ) with typecode |-
23 2 22 ax-mp 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 ) ) } ) ` (/) ) = { x | ( E. z e. (/) ( x = ( prop-. ` z ) \/ E. w e. (/) 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 ) ) } ) ` (/) ) = { x | ( E. z e. (/) ( x = ( prop-. ` z ) \/ E. w e. (/) x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } with typecode |-
24 14 23 eleqtrrdi Could not format ( n e. NN -> ( propvar ` n ) e. ( ( 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 |- ( n e. NN -> ( propvar ` n ) e. ( ( 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 |-
25 6 24 sseldd Could not format ( n e. NN -> ( propvar ` n ) e. PROP ) : No typesetting found for |- ( n e. NN -> ( propvar ` n ) e. PROP ) with typecode |-