Metamath Proof Explorer

Theorem reusngf

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

Ref Expression
Hypotheses rexsngf.1 ⊢Ⅎxψ
rexsngf.2 ⊢x=A→φ↔ψ
Assertion reusngf ⊢A∈V→∃!x∈Aφ↔ψ

Proof

Step Hyp Ref Expression
1 rexsngf.1 ⊢Ⅎxψ
2 rexsngf.2 ⊢x=A→φ↔ψ
3 nfsbc1v ⊢Ⅎx[˙c/x]˙φ
4 nfsbc1v ⊢Ⅎx[˙w/x]˙φ
5 sbceq1a ⊢x=w→φ↔[˙w/x]˙φ
6 dfsbcq ⊢w=c→[˙w/x]˙φ↔[˙c/x]˙φ
7 3 4 5 6 reu8nf ⊢∃!x∈Aφ↔∃x∈Aφ∧∀c∈A[˙c/x]˙φ→x=c
8 nfcv ⊢Ⅎ_xA
9 nfv ⊢ℲxA=c
10 3 9 nfim ⊢Ⅎx[˙c/x]˙φ→A=c
11 8 10 nfralw ⊢Ⅎx∀c∈A[˙c/x]˙φ→A=c
12 1 11 nfan ⊢Ⅎxψ∧∀c∈A[˙c/x]˙φ→A=c
13 eqeq1 ⊢x=A→x=c↔A=c
14 13 imbi2d ⊢x=A→[˙c/x]˙φ→x=c↔[˙c/x]˙φ→A=c
15 14 ralbidv ⊢x=A→∀c∈A[˙c/x]˙φ→x=c↔∀c∈A[˙c/x]˙φ→A=c
16 2 15 anbi12d ⊢x=A→φ∧∀c∈A[˙c/x]˙φ→x=c↔ψ∧∀c∈A[˙c/x]˙φ→A=c
17 12 16 rexsngf ⊢A∈V→∃x∈Aφ∧∀c∈A[˙c/x]˙φ→x=c↔ψ∧∀c∈A[˙c/x]˙φ→A=c
18 nfv ⊢Ⅎc[˙A/x]˙φ→A=A
19 dfsbcq ⊢c=A→[˙c/x]˙φ↔[˙A/x]˙φ
20 eqeq2 ⊢c=A→A=c↔A=A
21 19 20 imbi12d ⊢c=A→[˙c/x]˙φ→A=c↔[˙A/x]˙φ→A=A
22 18 21 ralsngf ⊢A∈V→∀c∈A[˙c/x]˙φ→A=c↔[˙A/x]˙φ→A=A
23 22 anbi2d ⊢A∈V→ψ∧∀c∈A[˙c/x]˙φ→A=c↔ψ∧[˙A/x]˙φ→A=A
24 eqidd ⊢[˙A/x]˙φ→A=A
25 24 biantru ⊢ψ↔ψ∧[˙A/x]˙φ→A=A
26 23 25 bitr4di ⊢A∈V→ψ∧∀c∈A[˙c/x]˙φ→A=c↔ψ
27 17 26 bitrd ⊢A∈V→∃x∈Aφ∧∀c∈A[˙c/x]˙φ→x=c↔ψ
28 7 27 bitrid ⊢A∈V→∃!x∈Aφ↔ψ