Metamath Proof Explorer

Theorem elpssmo

Description: Uniqueness of elements is equivalent to uniqueness of proper subsets. (Contributed by Adrian Ducourtial, 26-Oct-2026)

Ref Expression
Assertion elpssmo 
|- ( E* x x e. A <-> E* y y C. A )

Proof

Step Hyp Ref Expression
1 0ex 
 |-  (/) e. _V
2 1 a1i 
 |-  ( E* x x e. A -> (/) e. _V )
3 pssss 
 |-  ( y C. A -> y C_ A )
4 3 sseld 
 |-  ( y C. A -> ( v e. y -> v e. A ) )
5 4 alrimiv 
 |-  ( y C. A -> A. v ( v e. y -> v e. A ) )
6 eleq1w 
 |-  ( x = v -> ( x e. A <-> v e. A ) )
7 6 cbvmovw 
 |-  ( E* x x e. A <-> E* v v e. A )
8 dfmo 
 |-  ( E* v v e. A <-> E. z A. v ( v e. A -> v = z ) )
9 eleq1w 
 |-  ( v = w -> ( v e. A <-> w e. A ) )
10 equequ1 
 |-  ( v = w -> ( v = z <-> w = z ) )
11 9 10 imbi12d 
 |-  ( v = w -> ( ( v e. A -> v = z ) <-> ( w e. A -> w = z ) ) )
12 11 spvv 
 |-  ( A. v ( v e. A -> v = z ) -> ( w e. A -> w = z ) )
13 12 com12 
 |-  ( w e. A -> ( A. v ( v e. A -> v = z ) -> w = z ) )
14 equcomiv 
 |-  ( w = z -> z = w )
15 13 14 syl6 
 |-  ( w e. A -> ( A. v ( v e. A -> v = z ) -> z = w ) )
16 equequ2 
 |-  ( z = w -> ( v = z <-> v = w ) )
17 16 imbi2d 
 |-  ( z = w -> ( ( v e. A -> v = z ) <-> ( v e. A -> v = w ) ) )
18 17 albidv 
 |-  ( z = w -> ( A. v ( v e. A -> v = z ) <-> A. v ( v e. A -> v = w ) ) )
19 15 18 syl6 
 |-  ( w e. A -> ( A. v ( v e. A -> v = z ) -> ( A. v ( v e. A -> v = z ) <-> A. v ( v e. A -> v = w ) ) ) )
20 19 ibd 
 |-  ( w e. A -> ( A. v ( v e. A -> v = z ) -> A. v ( v e. A -> v = w ) ) )
21 20 com12 
 |-  ( A. v ( v e. A -> v = z ) -> ( w e. A -> A. v ( v e. A -> v = w ) ) )
22 21 exlimiv 
 |-  ( E. z A. v ( v e. A -> v = z ) -> ( w e. A -> A. v ( v e. A -> v = w ) ) )
23 8 22 sylbi 
 |-  ( E* v v e. A -> ( w e. A -> A. v ( v e. A -> v = w ) ) )
24 7 23 sylbi 
 |-  ( E* x x e. A -> ( w e. A -> A. v ( v e. A -> v = w ) ) )
25 elequ1 
 |-  ( v = w -> ( v e. y <-> w e. y ) )
26 25 notbid 
 |-  ( v = w -> ( -. v e. y <-> -. w e. y ) )
27 26 biimprcd 
 |-  ( -. w e. y -> ( v = w -> -. v e. y ) )
28 27 imim2d 
 |-  ( -. w e. y -> ( ( v e. A -> v = w ) -> ( v e. A -> -. v e. y ) ) )
29 28 alimdv 
 |-  ( -. w e. y -> ( A. v ( v e. A -> v = w ) -> A. v ( v e. A -> -. v e. y ) ) )
30 24 29 syl9 
 |-  ( E* x x e. A -> ( -. w e. y -> ( w e. A -> A. v ( v e. A -> -. v e. y ) ) ) )
31 30 impcomd 
 |-  ( E* x x e. A -> ( ( w e. A /\ -. w e. y ) -> A. v ( v e. A -> -. v e. y ) ) )
32 31 exlimdv 
 |-  ( E* x x e. A -> ( E. w ( w e. A /\ -. w e. y ) -> A. v ( v e. A -> -. v e. y ) ) )
33 pssnel 
 |-  ( y C. A -> E. w ( w e. A /\ -. w e. y ) )
34 32 33 impel 
 |-  ( ( E* x x e. A /\ y C. A ) -> A. v ( v e. A -> -. v e. y ) )
35 alsyl 
 |-  ( ( A. v ( v e. y -> v e. A ) /\ A. v ( v e. A -> -. v e. y ) ) -> A. v ( v e. y -> -. v e. y ) )
36 5 34 35 syl2an2 
 |-  ( ( E* x x e. A /\ y C. A ) -> A. v ( v e. y -> -. v e. y ) )
37 pm2.01 
 |-  ( ( v e. y -> -. v e. y ) -> -. v e. y )
38 36 37 sylg 
 |-  ( ( E* x x e. A /\ y C. A ) -> A. v -. v e. y )
39 eq0 
 |-  ( y = (/) <-> A. v -. v e. y )
40 38 39 sylibr 
 |-  ( ( E* x x e. A /\ y C. A ) -> y = (/) )
41 40 ex 
 |-  ( E* x x e. A -> ( y C. A -> y = (/) ) )
42 41 alrimiv 
 |-  ( E* x x e. A -> A. y ( y C. A -> y = (/) ) )
43 eqeq2 
 |-  ( u = (/) -> ( y = u <-> y = (/) ) )
44 43 imbi2d 
 |-  ( u = (/) -> ( ( y C. A -> y = u ) <-> ( y C. A -> y = (/) ) ) )
45 44 albidv 
 |-  ( u = (/) -> ( A. y ( y C. A -> y = u ) <-> A. y ( y C. A -> y = (/) ) ) )
46 2 42 45 spcedv 
 |-  ( E* x x e. A -> E. u A. y ( y C. A -> y = u ) )
47 dfmo 
 |-  ( E* y y C. A <-> E. u A. y ( y C. A -> y = u ) )
48 46 47 sylibr 
 |-  ( E* x x e. A -> E* y y C. A )
49 vsnid 
 |-  x e. { x }
50 49 n0ii 
 |-  -. { x } = (/)
51 simp1 
 |-  ( ( x e. A /\ v e. A /\ -. v = x ) -> x e. A )
52 velsn 
 |-  ( v e. { x } <-> v = x )
53 52 notbii 
 |-  ( -. v e. { x } <-> -. v = x )
54 ssnelpss 
 |-  ( { x } C_ A -> ( ( v e. A /\ -. v e. { x } ) -> { x } C. A ) )
55 snssi 
 |-  ( x e. A -> { x } C_ A )
56 54 55 syl11 
 |-  ( ( v e. A /\ -. v e. { x } ) -> ( x e. A -> { x } C. A ) )
57 53 56 sylan2br 
 |-  ( ( v e. A /\ -. v = x ) -> ( x e. A -> { x } C. A ) )
58 57 ex 
 |-  ( v e. A -> ( -. v = x -> ( x e. A -> { x } C. A ) ) )
59 58 com23 
 |-  ( v e. A -> ( x e. A -> ( -. v = x -> { x } C. A ) ) )
60 59 3imp21 
 |-  ( ( x e. A /\ v e. A /\ -. v = x ) -> { x } C. A )
61 noel 
 |-  -. x e. (/)
62 0ss 
 |-  (/) C_ A
63 ssnelpss 
 |-  ( (/) C_ A -> ( ( x e. A /\ -. x e. (/) ) -> (/) C. A ) )
64 62 63 ax-mp 
 |-  ( ( x e. A /\ -. x e. (/) ) -> (/) C. A )
65 61 64 mpan2 
 |-  ( x e. A -> (/) C. A )
66 psseq1 
 |-  ( y = w -> ( y C. A <-> w C. A ) )
67 66 mo4 
 |-  ( E* y y C. A <-> A. y A. w ( ( y C. A /\ w C. A ) -> y = w ) )
68 vsnex 
 |-  { x } e. _V
69 psseq1 
 |-  ( y = { x } -> ( y C. A <-> { x } C. A ) )
70 69 anbi1d 
 |-  ( y = { x } -> ( ( y C. A /\ w C. A ) <-> ( { x } C. A /\ w C. A ) ) )
71 eqeq1 
 |-  ( y = { x } -> ( y = w <-> { x } = w ) )
72 70 71 imbi12d 
 |-  ( y = { x } -> ( ( ( y C. A /\ w C. A ) -> y = w ) <-> ( ( { x } C. A /\ w C. A ) -> { x } = w ) ) )
73 72 albidv 
 |-  ( y = { x } -> ( A. w ( ( y C. A /\ w C. A ) -> y = w ) <-> A. w ( ( { x } C. A /\ w C. A ) -> { x } = w ) ) )
74 68 73 spcv 
 |-  ( A. y A. w ( ( y C. A /\ w C. A ) -> y = w ) -> A. w ( ( { x } C. A /\ w C. A ) -> { x } = w ) )
75 67 74 sylbi 
 |-  ( E* y y C. A -> A. w ( ( { x } C. A /\ w C. A ) -> { x } = w ) )
76 psseq1 
 |-  ( w = (/) -> ( w C. A <-> (/) C. A ) )
77 76 anbi2d 
 |-  ( w = (/) -> ( ( { x } C. A /\ w C. A ) <-> ( { x } C. A /\ (/) C. A ) ) )
78 eqeq2 
 |-  ( w = (/) -> ( { x } = w <-> { x } = (/) ) )
79 77 78 imbi12d 
 |-  ( w = (/) -> ( ( ( { x } C. A /\ w C. A ) -> { x } = w ) <-> ( ( { x } C. A /\ (/) C. A ) -> { x } = (/) ) ) )
80 1 79 spcv 
 |-  ( A. w ( ( { x } C. A /\ w C. A ) -> { x } = w ) -> ( ( { x } C. A /\ (/) C. A ) -> { x } = (/) ) )
81 75 80 syl 
 |-  ( E* y y C. A -> ( ( { x } C. A /\ (/) C. A ) -> { x } = (/) ) )
82 81 ancomsd 
 |-  ( E* y y C. A -> ( ( (/) C. A /\ { x } C. A ) -> { x } = (/) ) )
83 82 com12 
 |-  ( ( (/) C. A /\ { x } C. A ) -> ( E* y y C. A -> { x } = (/) ) )
84 65 83 sylan 
 |-  ( ( x e. A /\ { x } C. A ) -> ( E* y y C. A -> { x } = (/) ) )
85 51 60 84 syl2anc 
 |-  ( ( x e. A /\ v e. A /\ -. v = x ) -> ( E* y y C. A -> { x } = (/) ) )
86 85 3expia 
 |-  ( ( x e. A /\ v e. A ) -> ( -. v = x -> ( E* y y C. A -> { x } = (/) ) ) )
87 86 com23 
 |-  ( ( x e. A /\ v e. A ) -> ( E* y y C. A -> ( -. v = x -> { x } = (/) ) ) )
88 87 3impia 
 |-  ( ( x e. A /\ v e. A /\ E* y y C. A ) -> ( -. v = x -> { x } = (/) ) )
89 50 88 mt3i 
 |-  ( ( x e. A /\ v e. A /\ E* y y C. A ) -> v = x )
90 89 3comr 
 |-  ( ( E* y y C. A /\ x e. A /\ v e. A ) -> v = x )
91 90 equcomd 
 |-  ( ( E* y y C. A /\ x e. A /\ v e. A ) -> x = v )
92 91 3expib 
 |-  ( E* y y C. A -> ( ( x e. A /\ v e. A ) -> x = v ) )
93 92 alrimivv 
 |-  ( E* y y C. A -> A. x A. v ( ( x e. A /\ v e. A ) -> x = v ) )
94 6 mo4 
 |-  ( E* x x e. A <-> A. x A. v ( ( x e. A /\ v e. A ) -> x = v ) )
95 93 94 sylibr 
 |-  ( E* y y C. A -> E* x x e. A )
96 48 95 impbii 
 |-  ( E* x x e. A <-> E* y y C. A )