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 ⊢ Ⅎ _ x A
9 nfv ⊢ Ⅎ x A = 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 φ ↔ ψ