Metamath Proof Explorer


Theorem reusngf

Description: Restricted existential uniqueness over a singleton. (Contributed by AV, 3-Apr-2023)

Ref Expression
Hypotheses rexsngf.1
|- F/ x ps
rexsngf.2
|- ( x = A -> ( ph <-> ps ) )
Assertion reusngf
|- ( A e. V -> ( E! x e. { A } ph <-> ps ) )

Proof

Step Hyp Ref Expression
1 rexsngf.1
 |-  F/ x ps
2 rexsngf.2
 |-  ( x = A -> ( ph <-> ps ) )
3 nfsbc1v
 |-  F/ x [. c / x ]. ph
4 nfsbc1v
 |-  F/ x [. w / x ]. ph
5 sbceq1a
 |-  ( x = w -> ( ph <-> [. w / x ]. ph ) )
6 dfsbcq
 |-  ( w = c -> ( [. w / x ]. ph <-> [. c / x ]. ph ) )
7 3 4 5 6 reu8nf
 |-  ( E! x e. { A } ph <-> E. x e. { A } ( ph /\ A. c e. { A } ( [. c / x ]. ph -> x = c ) ) )
8 nfcv
 |-  F/_ x { A }
9 nfv
 |-  F/ x A = c
10 3 9 nfim
 |-  F/ x ( [. c / x ]. ph -> A = c )
11 8 10 nfralw
 |-  F/ x A. c e. { A } ( [. c / x ]. ph -> A = c )
12 1 11 nfan
 |-  F/ x ( ps /\ A. c e. { A } ( [. c / x ]. ph -> A = c ) )
13 eqeq1
 |-  ( x = A -> ( x = c <-> A = c ) )
14 13 imbi2d
 |-  ( x = A -> ( ( [. c / x ]. ph -> x = c ) <-> ( [. c / x ]. ph -> A = c ) ) )
15 14 ralbidv
 |-  ( x = A -> ( A. c e. { A } ( [. c / x ]. ph -> x = c ) <-> A. c e. { A } ( [. c / x ]. ph -> A = c ) ) )
16 2 15 anbi12d
 |-  ( x = A -> ( ( ph /\ A. c e. { A } ( [. c / x ]. ph -> x = c ) ) <-> ( ps /\ A. c e. { A } ( [. c / x ]. ph -> A = c ) ) ) )
17 12 16 rexsngf
 |-  ( A e. V -> ( E. x e. { A } ( ph /\ A. c e. { A } ( [. c / x ]. ph -> x = c ) ) <-> ( ps /\ A. c e. { A } ( [. c / x ]. ph -> A = c ) ) ) )
18 nfv
 |-  F/ c ( [. A / x ]. ph -> A = A )
19 dfsbcq
 |-  ( c = A -> ( [. c / x ]. ph <-> [. A / x ]. ph ) )
20 eqeq2
 |-  ( c = A -> ( A = c <-> A = A ) )
21 19 20 imbi12d
 |-  ( c = A -> ( ( [. c / x ]. ph -> A = c ) <-> ( [. A / x ]. ph -> A = A ) ) )
22 18 21 ralsngf
 |-  ( A e. V -> ( A. c e. { A } ( [. c / x ]. ph -> A = c ) <-> ( [. A / x ]. ph -> A = A ) ) )
23 22 anbi2d
 |-  ( A e. V -> ( ( ps /\ A. c e. { A } ( [. c / x ]. ph -> A = c ) ) <-> ( ps /\ ( [. A / x ]. ph -> A = A ) ) ) )
24 eqidd
 |-  ( [. A / x ]. ph -> A = A )
25 24 biantru
 |-  ( ps <-> ( ps /\ ( [. A / x ]. ph -> A = A ) ) )
26 23 25 bitr4di
 |-  ( A e. V -> ( ( ps /\ A. c e. { A } ( [. c / x ]. ph -> A = c ) ) <-> ps ) )
27 17 26 bitrd
 |-  ( A e. V -> ( E. x e. { A } ( ph /\ A. c e. { A } ( [. c / x ]. ph -> x = c ) ) <-> ps ) )
28 7 27 syl5bb
 |-  ( A e. V -> ( E! x e. { A } ph <-> ps ) )