Theorem pw1m 7355

Description: A truth value which is inhabited is equal to true. This is a variation of pwntru 4251 and pwtrufal 16075. (Contributed by Jim Kingdon, 10-Jan-2026.)

Assertion

Ref	Expression
pw1m	|- ( ( A e. ~P 1o /\ E. x x e. A ) -> A = 1o )

Distinct variable group:   x, A

Proof of Theorem pw1m

Step	Hyp	Ref	Expression
1		elpwi 3630	. . . . . . . 8 |- ( A e. ~P 1o -> A C_ 1o )
2		df1o2 6528	. . . . . . . 8 |- 1o = { (/) }
3	1, 2	sseqtrdi 3245	. . . . . . 7 |- ( A e. ~P 1o -> A C_ { (/) } )
4	3	adantr 276	. . . . . 6 |- ( ( A e. ~P 1o /\ x e. A ) -> A C_ { (/) } )
5	1	sselda 3197	. . . . . . . . . 10 |- ( ( A e. ~P 1o /\ x e. A ) -> x e. 1o )
6	5, 2	eleqtrdi 2299	. . . . . . . . 9 |- ( ( A e. ~P 1o /\ x e. A ) -> x e. { (/) } )
7		elsni 3656	. . . . . . . . 9 |- ( x e. { (/) } -> x = (/) )
8	6, 7	syl 14	. . . . . . . 8 |- ( ( A e. ~P 1o /\ x e. A ) -> x = (/) )
9		simpr 110	. . . . . . . 8 |- ( ( A e. ~P 1o /\ x e. A ) -> x e. A )
10	8, 9	eqeltrrd 2284	. . . . . . 7 |- ( ( A e. ~P 1o /\ x e. A ) -> (/) e. A )
11	10	snssd 3784	. . . . . 6 |- ( ( A e. ~P 1o /\ x e. A ) -> { (/) } C_ A )
12	4, 11	eqssd 3214	. . . . 5 |- ( ( A e. ~P 1o /\ x e. A ) -> A = { (/) } )
13	12, 2	eqtr4di 2257	. . . 4 |- ( ( A e. ~P 1o /\ x e. A ) -> A = 1o )
14	13	ex 115	. . 3 |- ( A e. ~P 1o -> ( x e. A -> A = 1o ) )
15	14	exlimdv 1843	. 2 |- ( A e. ~P 1o -> ( E. x x e. A -> A = 1o ) )
16	15	imp 124	1 |- ( ( A e. ~P 1o /\ E. x x e. A ) -> A = 1o )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1373   E.wex 1516   e. wcel 2177   C_ wss 3170   (/)c0 3464   ~Pcpw 3621   {csn 3638   1oc1o 6508

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-v 2775  df-dif 3172  df-un 3174  df-in 3176  df-ss 3183  df-nul 3465  df-pw 3623  df-sn 3644  df-suc 4426  df-1o 6515

This theorem is referenced by:  pw1if  7356