Metamath Proof Explorer

Theorem rexreusng

Description: Restricted existential uniqueness over a singleton is equivalent to a restricted existential quantification over a singleton. (Contributed by AV, 3-Apr-2023)

Ref Expression
Assertion rexreusng 
|- ( A e. V -> ( E. x e. { A } ph <-> E! x e. { A } ph ) )

Proof

Step Hyp Ref Expression
1 eqidd 
 |-  ( ( [. A / y ]. [. A / x ]. ph /\ [. A / x ]. ph ) -> A = A )
2 nfsbc1v 
 |-  F/ y [. A / y ]. [. A / x ]. ph
3 nfv 
 |-  F/ y [. A / x ]. ph
4 2 3 nfan 
 |-  F/ y ( [. A / y ]. [. A / x ]. ph /\ [. A / x ]. ph )
5 nfv 
 |-  F/ y A = A
6 4 5 nfim 
 |-  F/ y ( ( [. A / y ]. [. A / x ]. ph /\ [. A / x ]. ph ) -> A = A )
7 sbceq1a 
 |-  ( y = A -> ( [. A / x ]. ph <-> [. A / y ]. [. A / x ]. ph ) )
8 dfsbcq2 
 |-  ( y = A -> ( [ y / x ] ph <-> [. A / x ]. ph ) )
9 7 8 anbi12d 
 |-  ( y = A -> ( ( [. A / x ]. ph /\ [ y / x ] ph ) <-> ( [. A / y ]. [. A / x ]. ph /\ [. A / x ]. ph ) ) )
10 eqeq2 
 |-  ( y = A -> ( A = y <-> A = A ) )
11 9 10 imbi12d 
 |-  ( y = A -> ( ( ( [. A / x ]. ph /\ [ y / x ] ph ) -> A = y ) <-> ( ( [. A / y ]. [. A / x ]. ph /\ [. A / x ]. ph ) -> A = A ) ) )
12 6 11 ralsngf 
 |-  ( A e. V -> ( A. y e. { A } ( ( [. A / x ]. ph /\ [ y / x ] ph ) -> A = y ) <-> ( ( [. A / y ]. [. A / x ]. ph /\ [. A / x ]. ph ) -> A = A ) ) )
13 1 12 mpbiri 
 |-  ( A e. V -> A. y e. { A } ( ( [. A / x ]. ph /\ [ y / x ] ph ) -> A = y ) )
14 nfcv 
 |-  F/_ x { A }
15 nfsbc1v 
 |-  F/ x [. A / x ]. ph
16 nfs1v 
 |-  F/ x [ y / x ] ph
17 15 16 nfan 
 |-  F/ x ( [. A / x ]. ph /\ [ y / x ] ph )
18 nfv 
 |-  F/ x A = y
19 17 18 nfim 
 |-  F/ x ( ( [. A / x ]. ph /\ [ y / x ] ph ) -> A = y )
20 14 19 nfralw 
 |-  F/ x A. y e. { A } ( ( [. A / x ]. ph /\ [ y / x ] ph ) -> A = y )
21 sbceq1a 
 |-  ( x = A -> ( ph <-> [. A / x ]. ph ) )
22 21 anbi1d 
 |-  ( x = A -> ( ( ph /\ [ y / x ] ph ) <-> ( [. A / x ]. ph /\ [ y / x ] ph ) ) )
23 eqeq1 
 |-  ( x = A -> ( x = y <-> A = y ) )
24 22 23 imbi12d 
 |-  ( x = A -> ( ( ( ph /\ [ y / x ] ph ) -> x = y ) <-> ( ( [. A / x ]. ph /\ [ y / x ] ph ) -> A = y ) ) )
25 24 ralbidv 
 |-  ( x = A -> ( A. y e. { A } ( ( ph /\ [ y / x ] ph ) -> x = y ) <-> A. y e. { A } ( ( [. A / x ]. ph /\ [ y / x ] ph ) -> A = y ) ) )
26 20 25 ralsngf 
 |-  ( A e. V -> ( A. x e. { A } A. y e. { A } ( ( ph /\ [ y / x ] ph ) -> x = y ) <-> A. y e. { A } ( ( [. A / x ]. ph /\ [ y / x ] ph ) -> A = y ) ) )
27 13 26 mpbird 
 |-  ( A e. V -> A. x e. { A } A. y e. { A } ( ( ph /\ [ y / x ] ph ) -> x = y ) )
28 27 biantrud 
 |-  ( A e. V -> ( E. x e. { A } ph <-> ( E. x e. { A } ph /\ A. x e. { A } A. y e. { A } ( ( ph /\ [ y / x ] ph ) -> x = y ) ) ) )
29 reu2 
 |-  ( E! x e. { A } ph <-> ( E. x e. { A } ph /\ A. x e. { A } A. y e. { A } ( ( ph /\ [ y / x ] ph ) -> x = y ) ) )
30 28 29 bitr4di 
 |-  ( A e. V -> ( E. x e. { A } ph <-> E! x e. { A } ph ) )