Metamath Proof Explorer

Theorem dfprop1

Description: The set of variables encoded as a natural number, negations of sentences of propositional calculus, and implications between sentences of propositional calculus is a subset of PROP . (Contributed by Thomas van Maaren, 21-Aug-2026)

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

Proof

Step Hyp Ref Expression
1 simpr Could not format ( ( z e. PROP /\ x = ( prop-. ` z ) ) -> x = ( prop-. ` z ) ) : No typesetting found for |- ( ( z e. PROP /\ x = ( prop-. ` z ) ) -> x = ( prop-. ` z ) ) with typecode |-
2 negprop Could not format ( z e. PROP -> ( prop-. ` z ) e. PROP ) : No typesetting found for |- ( z e. PROP -> ( prop-. ` z ) e. PROP ) with typecode |-
3 2 adantr Could not format ( ( z e. PROP /\ x = ( prop-. ` z ) ) -> ( prop-. ` z ) e. PROP ) : No typesetting found for |- ( ( z e. PROP /\ x = ( prop-. ` z ) ) -> ( prop-. ` z ) e. PROP ) with typecode |-
4 1 3 eqeltrd Could not format ( ( z e. PROP /\ x = ( prop-. ` z ) ) -> x e. PROP ) : No typesetting found for |- ( ( z e. PROP /\ x = ( prop-. ` z ) ) -> x e. PROP ) with typecode |-
5 df-rex Could not format ( E. w e. PROP x = ( w prop-> z ) <-> E. w ( w e. PROP /\ x = ( w prop-> z ) ) ) : No typesetting found for |- ( E. w e. PROP x = ( w prop-> z ) <-> E. w ( w e. PROP /\ x = ( w prop-> z ) ) ) with typecode |-
6 5 anbi2i Could not format ( ( z e. PROP /\ E. w e. PROP x = ( w prop-> z ) ) <-> ( z e. PROP /\ E. w ( w e. PROP /\ x = ( w prop-> z ) ) ) ) : No typesetting found for |- ( ( z e. PROP /\ E. w e. PROP x = ( w prop-> z ) ) <-> ( z e. PROP /\ E. w ( w e. PROP /\ x = ( w prop-> z ) ) ) ) with typecode |-
7 19.42v Could not format ( E. w ( z e. PROP /\ ( w e. PROP /\ x = ( w prop-> z ) ) ) <-> ( z e. PROP /\ E. w ( w e. PROP /\ x = ( w prop-> z ) ) ) ) : No typesetting found for |- ( E. w ( z e. PROP /\ ( w e. PROP /\ x = ( w prop-> z ) ) ) <-> ( z e. PROP /\ E. w ( w e. PROP /\ x = ( w prop-> z ) ) ) ) with typecode |-
8 6 7 bitr4i Could not format ( ( z e. PROP /\ E. w e. PROP x = ( w prop-> z ) ) <-> E. w ( z e. PROP /\ ( w e. PROP /\ x = ( w prop-> z ) ) ) ) : No typesetting found for |- ( ( z e. PROP /\ E. w e. PROP x = ( w prop-> z ) ) <-> E. w ( z e. PROP /\ ( w e. PROP /\ x = ( w prop-> z ) ) ) ) with typecode |-
9 simprr Could not format ( ( z e. PROP /\ ( w e. PROP /\ x = ( w prop-> z ) ) ) -> x = ( w prop-> z ) ) : No typesetting found for |- ( ( z e. PROP /\ ( w e. PROP /\ x = ( w prop-> z ) ) ) -> x = ( w prop-> z ) ) with typecode |-
10 simpl Could not format ( ( w e. PROP /\ x = ( w prop-> z ) ) -> w e. PROP ) : No typesetting found for |- ( ( w e. PROP /\ x = ( w prop-> z ) ) -> w e. PROP ) with typecode |-
11 simpl Could not format ( ( z e. PROP /\ ( w e. PROP /\ x = ( w prop-> z ) ) ) -> z e. PROP ) : No typesetting found for |- ( ( z e. PROP /\ ( w e. PROP /\ x = ( w prop-> z ) ) ) -> z e. PROP ) with typecode |-
12 impprop Could not format ( ( w e. PROP /\ z e. PROP ) -> ( w prop-> z ) e. PROP ) : No typesetting found for |- ( ( w e. PROP /\ z e. PROP ) -> ( w prop-> z ) e. PROP ) with typecode |-
13 10 11 12 syl2an2 Could not format ( ( z e. PROP /\ ( w e. PROP /\ x = ( w prop-> z ) ) ) -> ( w prop-> z ) e. PROP ) : No typesetting found for |- ( ( z e. PROP /\ ( w e. PROP /\ x = ( w prop-> z ) ) ) -> ( w prop-> z ) e. PROP ) with typecode |-
14 9 13 eqeltrd Could not format ( ( z e. PROP /\ ( w e. PROP /\ x = ( w prop-> z ) ) ) -> x e. PROP ) : No typesetting found for |- ( ( z e. PROP /\ ( w e. PROP /\ x = ( w prop-> z ) ) ) -> x e. PROP ) with typecode |-
15 14 exlimiv Could not format ( E. w ( z e. PROP /\ ( w e. PROP /\ x = ( w prop-> z ) ) ) -> x e. PROP ) : No typesetting found for |- ( E. w ( z e. PROP /\ ( w e. PROP /\ x = ( w prop-> z ) ) ) -> x e. PROP ) with typecode |-
16 8 15 sylbi Could not format ( ( z e. PROP /\ E. w e. PROP x = ( w prop-> z ) ) -> x e. PROP ) : No typesetting found for |- ( ( z e. PROP /\ E. w e. PROP x = ( w prop-> z ) ) -> x e. PROP ) with typecode |-
17 4 16 jaodan Could not format ( ( z e. PROP /\ ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) ) -> x e. PROP ) : No typesetting found for |- ( ( z e. PROP /\ ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) ) -> x e. PROP ) with typecode |-
18 17 rexlimiva Could not format ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) -> x e. PROP ) : No typesetting found for |- ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) -> x e. PROP ) with typecode |-
19 simpr Could not format ( ( n e. NN /\ x = ( propvar ` n ) ) -> x = ( propvar ` n ) ) : No typesetting found for |- ( ( n e. NN /\ x = ( propvar ` n ) ) -> x = ( propvar ` n ) ) with typecode |-
20 varprop Could not format ( n e. NN -> ( propvar ` n ) e. PROP ) : No typesetting found for |- ( n e. NN -> ( propvar ` n ) e. PROP ) with typecode |-
21 20 adantr Could not format ( ( n e. NN /\ x = ( propvar ` n ) ) -> ( propvar ` n ) e. PROP ) : No typesetting found for |- ( ( n e. NN /\ x = ( propvar ` n ) ) -> ( propvar ` n ) e. PROP ) with typecode |-
22 19 21 eqeltrd Could not format ( ( n e. NN /\ x = ( propvar ` n ) ) -> x e. PROP ) : No typesetting found for |- ( ( n e. NN /\ x = ( propvar ` n ) ) -> x e. PROP ) with typecode |-
23 22 rexlimiva Could not format ( E. n e. NN x = ( propvar ` n ) -> x e. PROP ) : No typesetting found for |- ( E. n e. NN x = ( propvar ` n ) -> x e. PROP ) with typecode |-
24 18 23 jaoi Could not format ( ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) -> x e. PROP ) : No typesetting found for |- ( ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) -> x e. PROP ) with typecode |-
25 24 abssi 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 |-