Theorem negprop

Description: The negation of a sentence of propositional calculus is a sentence of propositional calculus. (Contributed by Thomas van Maaren, 21-Aug-2026)

	Ref	Expression
Assertion	negprop	Could not format assertion : No typesetting found for |- ( x e. PROP -> ( prop-. ` x ) e. PROP ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-prop	Could not format PROP = setrecs ( ( y e. _V |-> { u | ( E. z e. y ( u = ( prop-. ` z ) \/ E. w e. y u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) } ) ) : No typesetting found for |- PROP = setrecs ( ( y e. _V |-> { u | ( E. z e. y ( u = ( prop-. ` z ) \/ E. w e. y u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) } ) ) with typecode |-
2		snexg	Could not format ( x e. PROP -> { x } e. _V ) : No typesetting found for |- ( x e. PROP -> { x } e. _V ) with typecode |-
3		snssi	Could not format ( x e. PROP -> { x } C_ PROP ) : No typesetting found for |- ( x e. PROP -> { x } C_ PROP ) with typecode |-
4	1 2 3	setrec1	Could not format ( x e. PROP -> ( ( y e. _V |-> { u | ( E. z e. y ( u = ( prop-. ` z ) \/ E. w e. y u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) } ) ` { x } ) C_ PROP ) : No typesetting found for |- ( x e. PROP -> ( ( y e. _V |-> { u | ( E. z e. y ( u = ( prop-. ` z ) \/ E. w e. y u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) } ) ` { x } ) C_ PROP ) with typecode |-
5		velsn	$$⊢z\in \left\{x\right\}\leftrightarrow z=x$$
6	5	anbi1i	Could not format ( ( z e. { x } /\ u = ( prop-. ` z ) ) <-> ( z = x /\ u = ( prop-. ` z ) ) ) : No typesetting found for |- ( ( z e. { x } /\ u = ( prop-. ` z ) ) <-> ( z = x /\ u = ( prop-. ` z ) ) ) with typecode |-
7	6	exbii	Could not format ( E. z ( z e. { x } /\ u = ( prop-. ` z ) ) <-> E. z ( z = x /\ u = ( prop-. ` z ) ) ) : No typesetting found for |- ( E. z ( z e. { x } /\ u = ( prop-. ` z ) ) <-> E. z ( z = x /\ u = ( prop-. ` z ) ) ) with typecode |-
8		fveq2	Could not format ( z = x -> ( prop-. ` z ) = ( prop-. ` x ) ) : No typesetting found for |- ( z = x -> ( prop-. ` z ) = ( prop-. ` x ) ) with typecode |-
9	8	eqeq2d	Could not format ( z = x -> ( u = ( prop-. ` z ) <-> u = ( prop-. ` x ) ) ) : No typesetting found for |- ( z = x -> ( u = ( prop-. ` z ) <-> u = ( prop-. ` x ) ) ) with typecode |-
10	9	equsexvw	Could not format ( E. z ( z = x /\ u = ( prop-. ` z ) ) <-> u = ( prop-. ` x ) ) : No typesetting found for |- ( E. z ( z = x /\ u = ( prop-. ` z ) ) <-> u = ( prop-. ` x ) ) with typecode |-
11	7 10	bitri	Could not format ( E. z ( z e. { x } /\ u = ( prop-. ` z ) ) <-> u = ( prop-. ` x ) ) : No typesetting found for |- ( E. z ( z e. { x } /\ u = ( prop-. ` z ) ) <-> u = ( prop-. ` x ) ) with typecode |-
12	11	bilanri	Could not format ( ( x e. PROP /\ u = ( prop-. ` x ) ) -> E. z ( z e. { x } /\ u = ( prop-. ` z ) ) ) : No typesetting found for |- ( ( x e. PROP /\ u = ( prop-. ` x ) ) -> E. z ( z e. { x } /\ u = ( prop-. ` z ) ) ) with typecode |-
13		df-rex	Could not format ( E. z e. { x } u = ( prop-. ` z ) <-> E. z ( z e. { x } /\ u = ( prop-. ` z ) ) ) : No typesetting found for |- ( E. z e. { x } u = ( prop-. ` z ) <-> E. z ( z e. { x } /\ u = ( prop-. ` z ) ) ) with typecode |-
14	13	biimpri	Could not format ( E. z ( z e. { x } /\ u = ( prop-. ` z ) ) -> E. z e. { x } u = ( prop-. ` z ) ) : No typesetting found for |- ( E. z ( z e. { x } /\ u = ( prop-. ` z ) ) -> E. z e. { x } u = ( prop-. ` z ) ) with typecode |-
15		orc	Could not format ( u = ( prop-. ` z ) -> ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) ) : No typesetting found for |- ( u = ( prop-. ` z ) -> ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) ) with typecode |-
16	15	reximi	Could not format ( E. z e. { x } u = ( prop-. ` z ) -> E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) ) : No typesetting found for |- ( E. z e. { x } u = ( prop-. ` z ) -> E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) ) with typecode |-
17	16	orcd	Could not format ( E. z e. { x } u = ( prop-. ` z ) -> ( E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) ) : No typesetting found for |- ( E. z e. { x } u = ( prop-. ` z ) -> ( E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) ) with typecode |-
18	12 14 17	3syl	Could not format ( ( x e. PROP /\ u = ( prop-. ` x ) ) -> ( E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) ) : No typesetting found for |- ( ( x e. PROP /\ u = ( prop-. ` x ) ) -> ( E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) ) with typecode |-
19	18	ex	Could not format ( x e. PROP -> ( u = ( prop-. ` x ) -> ( E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) ) ) : No typesetting found for |- ( x e. PROP -> ( u = ( prop-. ` x ) -> ( E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) ) ) with typecode |-
20	19	alrimiv	Could not format ( x e. PROP -> A. u ( u = ( prop-. ` x ) -> ( E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) ) ) : No typesetting found for |- ( x e. PROP -> A. u ( u = ( prop-. ` x ) -> ( E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) ) ) with typecode |-
21		fvex	Could not format ( prop-. ` x ) e. _V : No typesetting found for |- ( prop-. ` x ) e. _V with typecode |-
22		elab6g	Could not format ( ( prop-. ` x ) e. _V -> ( ( prop-. ` x ) e. { u | ( E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) } <-> A. u ( u = ( prop-. ` x ) -> ( E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) ) ) ) : No typesetting found for |- ( ( prop-. ` x ) e. _V -> ( ( prop-. ` x ) e. { u | ( E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) } <-> A. u ( u = ( prop-. ` x ) -> ( E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) ) ) ) with typecode |-
23	21 22	ax-mp	Could not format ( ( prop-. ` x ) e. { u | ( E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) } <-> A. u ( u = ( prop-. ` x ) -> ( E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) ) ) : No typesetting found for |- ( ( prop-. ` x ) e. { u | ( E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) } <-> A. u ( u = ( prop-. ` x ) -> ( E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) ) ) with typecode |-
24	20 23	sylibr	Could not format ( x e. PROP -> ( prop-. ` x ) e. { u | ( E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) } ) : No typesetting found for |- ( x e. PROP -> ( prop-. ` x ) e. { u | ( E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) } ) with typecode |-
25		vsnex	$$⊢\left\{x\right\}\in \mathrm{V}$$
26		rexeq	Could not format ( y = { x } -> ( E. w e. y u = ( w prop-> z ) <-> E. w e. { x } u = ( w prop-> z ) ) ) : No typesetting found for |- ( y = { x } -> ( E. w e. y u = ( w prop-> z ) <-> E. w e. { x } u = ( w prop-> z ) ) ) with typecode |-
27	26	orbi2d	Could not format ( y = { x } -> ( ( u = ( prop-. ` z ) \/ E. w e. y u = ( w prop-> z ) ) <-> ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) ) ) : No typesetting found for |- ( y = { x } -> ( ( u = ( prop-. ` z ) \/ E. w e. y u = ( w prop-> z ) ) <-> ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) ) ) with typecode |-
28	27	rexeqbi1dv	Could not format ( y = { x } -> ( E. z e. y ( u = ( prop-. ` z ) \/ E. w e. y u = ( w prop-> z ) ) <-> E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) ) ) : No typesetting found for |- ( y = { x } -> ( E. z e. y ( u = ( prop-. ` z ) \/ E. w e. y u = ( w prop-> z ) ) <-> E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) ) ) with typecode |-
29	28	orbi1d	Could not format ( y = { x } -> ( ( E. z e. y ( u = ( prop-. ` z ) \/ E. w e. y u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) <-> ( E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) ) ) : No typesetting found for |- ( y = { x } -> ( ( E. z e. y ( u = ( prop-. ` z ) \/ E. w e. y u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) <-> ( E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) ) ) with typecode |-
30	29	abbidv	Could not format ( y = { x } -> { u | ( E. z e. y ( u = ( prop-. ` z ) \/ E. w e. y u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) } = { u | ( E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) } ) : No typesetting found for |- ( y = { x } -> { u | ( E. z e. y ( u = ( prop-. ` z ) \/ E. w e. y u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) } = { u | ( E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) } ) with typecode |-
31		eqid	Could not format ( y e. _V |-> { u | ( E. z e. y ( u = ( prop-. ` z ) \/ E. w e. y u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) } ) = ( y e. _V |-> { u | ( E. z e. y ( u = ( prop-. ` z ) \/ E. w e. y u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) } ) : No typesetting found for |- ( y e. _V |-> { u | ( E. z e. y ( u = ( prop-. ` z ) \/ E. w e. y u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) } ) = ( y e. _V |-> { u | ( E. z e. y ( u = ( prop-. ` z ) \/ E. w e. y u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) } ) with typecode |-
32	25	dfproplem	Could not format { u | ( E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) } e. _V : No typesetting found for |- { u | ( E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) } e. _V with typecode |-
33	30 31 32	fvmpt	Could not format ( { x } e. _V -> ( ( y e. _V |-> { u | ( E. z e. y ( u = ( prop-. ` z ) \/ E. w e. y u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) } ) ` { x } ) = { u | ( E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) } ) : No typesetting found for |- ( { x } e. _V -> ( ( y e. _V |-> { u | ( E. z e. y ( u = ( prop-. ` z ) \/ E. w e. y u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) } ) ` { x } ) = { u | ( E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) } ) with typecode |-
34	25 33	ax-mp	Could not format ( ( y e. _V |-> { u | ( E. z e. y ( u = ( prop-. ` z ) \/ E. w e. y u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) } ) ` { x } ) = { u | ( E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) } : No typesetting found for |- ( ( y e. _V |-> { u | ( E. z e. y ( u = ( prop-. ` z ) \/ E. w e. y u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) } ) ` { x } ) = { u | ( E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) } with typecode |-
35	24 34	eleqtrrdi	Could not format ( x e. PROP -> ( prop-. ` x ) e. ( ( y e. _V |-> { u | ( E. z e. y ( u = ( prop-. ` z ) \/ E. w e. y u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) } ) ` { x } ) ) : No typesetting found for |- ( x e. PROP -> ( prop-. ` x ) e. ( ( y e. _V |-> { u | ( E. z e. y ( u = ( prop-. ` z ) \/ E. w e. y u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) } ) ` { x } ) ) with typecode |-
36	4 35	sseldd	Could not format ( x e. PROP -> ( prop-. ` x ) e. PROP ) : No typesetting found for |- ( x e. PROP -> ( prop-. ` x ) e. PROP ) with typecode |-