Theorem stnot 17039

Description: A proposition is double negation stable if and only if it is equivalent to a negated proposition. Here by "proposition" we mean a subset of a singleton (which is a choice which allows us to quantify over them). Posed as an exercise online by Yannick Forster. (Contributed by Jim Kingdon, 24-Jul-2026.)

Assertion

Ref	Expression
stnot	|- ( A e. ~P 1o -> ( ( -. -. A = 1o -> A = 1o ) <-> E. y e. ~P 1o ( A = 1o <-> -. y = 1o ) ) )

Distinct variable group:   y, A

Proof of Theorem stnot

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqeq1 2245	. . . . . 6 |- ( y = { x e. 1o | -. A = 1o } -> ( y = 1o <-> { x e. 1o | -. A = 1o } = 1o ) )
2	1	notbid 677	. . . . 5 |- ( y = { x e. 1o | -. A = 1o } -> ( -. y = 1o <-> -. { x e. 1o | -. A = 1o } = 1o ) )
3	2	bibi2d 232	. . . 4 |- ( y = { x e. 1o | -. A = 1o } -> ( ( A = 1o <-> -. y = 1o ) <-> ( A = 1o <-> -. { x e. 1o | -. A = 1o } = 1o ) ) )
4		1oex 6695	. . . . . 6 |- 1o e. _V
5		ssrab2 3333	. . . . . 6 |- { x e. 1o | -. A = 1o } C_ 1o
6	4, 5	elpwi2 4294	. . . . 5 |- { x e. 1o | -. A = 1o } e. ~P 1o
7	6	a1i 9	. . . 4 |- ( ( A e. ~P 1o /\ ( -. -. A = 1o -> A = 1o ) ) -> { x e. 1o | -. A = 1o } e. ~P 1o )
8		notnot 638	. . . . . 6 |- ( A = 1o -> -. -. A = 1o )
9		simpr 110	. . . . . 6 |- ( ( A e. ~P 1o /\ ( -. -. A = 1o -> A = 1o ) ) -> ( -. -. A = 1o -> A = 1o ) )
10	8, 9	impbid2 143	. . . . 5 |- ( ( A e. ~P 1o /\ ( -. -. A = 1o -> A = 1o ) ) -> ( A = 1o <-> -. -. A = 1o ) )
11		rabid2 2729	. . . . . . . . 9 |- ( 1o = { x e. 1o | -. A = 1o } <-> A. x e. 1o -. A = 1o )
12		eqcom 2240	. . . . . . . . 9 |- ( { x e. 1o | -. A = 1o } = 1o <-> 1o = { x e. 1o | -. A = 1o } )
13		0lt1o 6713	. . . . . . . . . 10 |- (/) e. 1o
14		elex2 2838	. . . . . . . . . 10 |- ( (/) e. 1o -> E. w w e. 1o )
15		r19.3rmv 3618	. . . . . . . . . 10 |- ( E. w w e. 1o -> ( -. A = 1o <-> A. x e. 1o -. A = 1o ) )
16	13, 14, 15	mp2b 8	. . . . . . . . 9 |- ( -. A = 1o <-> A. x e. 1o -. A = 1o )
17	11, 12, 16	3bitr4ri 213	. . . . . . . 8 |- ( -. A = 1o <-> { x e. 1o | -. A = 1o } = 1o )
18	17	a1i 9	. . . . . . 7 |- ( A e. ~P 1o -> ( -. A = 1o <-> { x e. 1o | -. A = 1o } = 1o ) )
19	18	notbid 677	. . . . . 6 |- ( A e. ~P 1o -> ( -. -. A = 1o <-> -. { x e. 1o | -. A = 1o } = 1o ) )
20	19	adantr 276	. . . . 5 |- ( ( A e. ~P 1o /\ ( -. -. A = 1o -> A = 1o ) ) -> ( -. -. A = 1o <-> -. { x e. 1o | -. A = 1o } = 1o ) )
21	10, 20	bitrd 188	. . . 4 |- ( ( A e. ~P 1o /\ ( -. -. A = 1o -> A = 1o ) ) -> ( A = 1o <-> -. { x e. 1o | -. A = 1o } = 1o ) )
22	3, 7, 21	rspcedvdw 2936	. . 3 |- ( ( A e. ~P 1o /\ ( -. -. A = 1o -> A = 1o ) ) -> E. y e. ~P 1o ( A = 1o <-> -. y = 1o ) )
23	22	ex 115	. 2 |- ( A e. ~P 1o -> ( ( -. -. A = 1o -> A = 1o ) -> E. y e. ~P 1o ( A = 1o <-> -. y = 1o ) ) )
24		simpr 110	. . . . . . 7 |- ( ( ( ( A e. ~P 1o /\ y e. ~P 1o ) /\ ( A = 1o <-> -. y = 1o ) ) /\ -. -. A = 1o ) -> -. -. A = 1o )
25		simplr 533	. . . . . . . 8 |- ( ( ( ( A e. ~P 1o /\ y e. ~P 1o ) /\ ( A = 1o <-> -. y = 1o ) ) /\ -. -. A = 1o ) -> ( A = 1o <-> -. y = 1o ) )
26	25	notbid 677	. . . . . . 7 |- ( ( ( ( A e. ~P 1o /\ y e. ~P 1o ) /\ ( A = 1o <-> -. y = 1o ) ) /\ -. -. A = 1o ) -> ( -. A = 1o <-> -. -. y = 1o ) )
27	24, 26	mtbid 683	. . . . . 6 |- ( ( ( ( A e. ~P 1o /\ y e. ~P 1o ) /\ ( A = 1o <-> -. y = 1o ) ) /\ -. -. A = 1o ) -> -. -. -. y = 1o )
28		notnotnot 643	. . . . . 6 |- ( -. -. -. y = 1o <-> -. y = 1o )
29	27, 28	sylib 122	. . . . 5 |- ( ( ( ( A e. ~P 1o /\ y e. ~P 1o ) /\ ( A = 1o <-> -. y = 1o ) ) /\ -. -. A = 1o ) -> -. y = 1o )
30	29, 25	mpbird 167	. . . 4 |- ( ( ( ( A e. ~P 1o /\ y e. ~P 1o ) /\ ( A = 1o <-> -. y = 1o ) ) /\ -. -. A = 1o ) -> A = 1o )
31	30	ex 115	. . 3 |- ( ( ( A e. ~P 1o /\ y e. ~P 1o ) /\ ( A = 1o <-> -. y = 1o ) ) -> ( -. -. A = 1o -> A = 1o ) )
32	31	rexlimdva2 2671	. 2 |- ( A e. ~P 1o -> ( E. y e. ~P 1o ( A = 1o <-> -. y = 1o ) -> ( -. -. A = 1o -> A = 1o ) ) )
33	23, 32	impbid 129	1 |- ( A e. ~P 1o -> ( ( -. -. A = 1o -> A = 1o ) <-> E. y e. ~P 1o ( A = 1o <-> -. y = 1o ) ) )

This proof depends on syntax axioms:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1402   E.wex 1545   e. wcel 2209   A.wral 2528   E.wrex 2529   {crab 2532   _Vcvv 2821   (/)c0 3520   ~Pcpw 3688   1oc1o 6680

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4249  ax-nul 4259  ax-pow 4311  ax-pr 4346  ax-un 4578

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-rab 2537  df-v 2823  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-nul 3521  df-pw 3690  df-sn 3715  df-pr 3716  df-uni 3936  df-tr 4230  df-iord 4511  df-on 4513  df-suc 4516  df-1o 6687

This theorem is used by: (None)