This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 bitrid 
 |-  ( A e. V -> ( E! x e. { A } ph <-> ps ) )