Metamath Proof Explorer

Theorem reu8

Description: Restricted uniqueness using implicit substitution. (Contributed by NM, 24-Oct-2006)

Ref Expression
Hypothesis rmo4.1 ⊢ x = y → φ ↔ ψ
Assertion reu8 ⊢ ∃! x ∈ A φ ↔ ∃ x ∈ A φ ∧ ∀ y ∈ A ψ → x = y

Proof

Step Hyp Ref Expression
1 rmo4.1 ⊢ x = y → φ ↔ ψ
2 1 cbvreuvw ⊢ ∃! x ∈ A φ ↔ ∃! y ∈ A ψ
3 reu6 ⊢ ∃! y ∈ A ψ ↔ ∃ x ∈ A ∀ y ∈ A ψ ↔ y = x
4 dfbi2 ⊢ ψ ↔ y = x ↔ ψ → y = x ∧ y = x → ψ
5 4 ralbii ⊢ ∀ y ∈ A ψ ↔ y = x ↔ ∀ y ∈ A ψ → y = x ∧ y = x → ψ
6 ancom ⊢ φ ∧ ∀ y ∈ A ψ → x = y ↔ ∀ y ∈ A ψ → x = y ∧ φ
7 equcom ⊢ x = y ↔ y = x
8 7 imbi2i ⊢ ψ → x = y ↔ ψ → y = x
9 8 ralbii ⊢ ∀ y ∈ A ψ → x = y ↔ ∀ y ∈ A ψ → y = x
10 9 a1i ⊢ x ∈ A → ∀ y ∈ A ψ → x = y ↔ ∀ y ∈ A ψ → y = x
11 biimt ⊢ x ∈ A → φ ↔ x ∈ A → φ
12 df-ral ⊢ ∀ y ∈ A y = x → ψ ↔ ∀ y y ∈ A → y = x → ψ
13 bi2.04 ⊢ y ∈ A → y = x → ψ ↔ y = x → y ∈ A → ψ
14 13 albii ⊢ ∀ y y ∈ A → y = x → ψ ↔ ∀ y y = x → y ∈ A → ψ
15 eleq1w ⊢ x = y → x ∈ A ↔ y ∈ A
16 15 1 imbi12d ⊢ x = y → x ∈ A → φ ↔ y ∈ A → ψ
17 16 bicomd ⊢ x = y → y ∈ A → ψ ↔ x ∈ A → φ
18 17 equcoms ⊢ y = x → y ∈ A → ψ ↔ x ∈ A → φ
19 18 equsalvw ⊢ ∀ y y = x → y ∈ A → ψ ↔ x ∈ A → φ
20 12 14 19 3bitrri ⊢ x ∈ A → φ ↔ ∀ y ∈ A y = x → ψ
21 11 20 syl6bb ⊢ x ∈ A → φ ↔ ∀ y ∈ A y = x → ψ
22 10 21 anbi12d ⊢ x ∈ A → ∀ y ∈ A ψ → x = y ∧ φ ↔ ∀ y ∈ A ψ → y = x ∧ ∀ y ∈ A y = x → ψ
23 6 22 syl5bb ⊢ x ∈ A → φ ∧ ∀ y ∈ A ψ → x = y ↔ ∀ y ∈ A ψ → y = x ∧ ∀ y ∈ A y = x → ψ
24 r19.26 ⊢ ∀ y ∈ A ψ → y = x ∧ y = x → ψ ↔ ∀ y ∈ A ψ → y = x ∧ ∀ y ∈ A y = x → ψ
25 23 24 syl6rbbr ⊢ x ∈ A → ∀ y ∈ A ψ → y = x ∧ y = x → ψ ↔ φ ∧ ∀ y ∈ A ψ → x = y
26 5 25 syl5bb ⊢ x ∈ A → ∀ y ∈ A ψ ↔ y = x ↔ φ ∧ ∀ y ∈ A ψ → x = y
27 26 rexbiia ⊢ ∃ x ∈ A ∀ y ∈ A ψ ↔ y = x ↔ ∃ x ∈ A φ ∧ ∀ y ∈ A ψ → x = y
28 2 3 27 3bitri ⊢ ∃! x ∈ A φ ↔ ∃ x ∈ A φ ∧ ∀ y ∈ A ψ → x = y