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

Metamath Proof Explorer

Theorem reu8nf

Description: Restricted uniqueness using implicit substitution. This version of reu8 uses a nonfreeness hypothesis for x and ps instead of distinct variable conditions. (Contributed by AV, 21-Jan-2022)

Ref Expression
Hypotheses reu8nf.1 ⊢ Ⅎ x ψ
reu8nf.2 ⊢ Ⅎ x χ
reu8nf.3 ⊢ x = w → φ ↔ χ
reu8nf.4 ⊢ w = y → χ ↔ ψ
Assertion reu8nf ⊢ ∃! x ∈ A φ ↔ ∃ x ∈ A φ ∧ ∀ y ∈ A ψ → x = y

Proof

Step Hyp Ref Expression
1 reu8nf.1 ⊢ Ⅎ x ψ
2 reu8nf.2 ⊢ Ⅎ x χ
3 reu8nf.3 ⊢ x = w → φ ↔ χ
4 reu8nf.4 ⊢ w = y → χ ↔ ψ
5 nfv ⊢ Ⅎ w φ
6 5 2 3 cbvreuw ⊢ ∃! x ∈ A φ ↔ ∃! w ∈ A χ
7 4 reu8 ⊢ ∃! w ∈ A χ ↔ ∃ w ∈ A χ ∧ ∀ y ∈ A ψ → w = y
8 nfcv ⊢ Ⅎ _ x A
9 nfv ⊢ Ⅎ x w = y
10 1 9 nfim ⊢ Ⅎ x ψ → w = y
11 8 10 nfralw ⊢ Ⅎ x ∀ y ∈ A ψ → w = y
12 2 11 nfan ⊢ Ⅎ x χ ∧ ∀ y ∈ A ψ → w = y
13 nfv ⊢ Ⅎ w φ ∧ ∀ y ∈ A ψ → x = y
14 3 bicomd ⊢ x = w → χ ↔ φ
15 14 equcoms ⊢ w = x → χ ↔ φ
16 equequ1 ⊢ w = x → w = y ↔ x = y
17 16 imbi2d ⊢ w = x → ψ → w = y ↔ ψ → x = y
18 17 ralbidv ⊢ w = x → ∀ y ∈ A ψ → w = y ↔ ∀ y ∈ A ψ → x = y
19 15 18 anbi12d ⊢ w = x → χ ∧ ∀ y ∈ A ψ → w = y ↔ φ ∧ ∀ y ∈ A ψ → x = y
20 12 13 19 cbvrexw ⊢ ∃ w ∈ A χ ∧ ∀ y ∈ A ψ → w = y ↔ ∃ x ∈ A φ ∧ ∀ y ∈ A ψ → x = y
21 6 7 20 3bitri ⊢ ∃! x ∈ A φ ↔ ∃ x ∈ A φ ∧ ∀ y ∈ A ψ → x = y