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 r19.26 ⊢ ∀ y ∈ A ψ → y = x ∧ y = x → ψ ↔ ∀ y ∈ A ψ → y = x ∧ ∀ y ∈ A y = x → ψ
7 ancom ⊢ φ ∧ ∀ y ∈ A ψ → x = y ↔ ∀ y ∈ A ψ → x = y ∧ φ
8 equcom ⊢ x = y ↔ y = x
9 8 imbi2i ⊢ ψ → x = y ↔ ψ → y = x
10 9 ralbii ⊢ ∀ y ∈ A ψ → x = y ↔ ∀ y ∈ A ψ → y = x
11 10 a1i ⊢ x ∈ A → ∀ y ∈ A ψ → x = y ↔ ∀ y ∈ A ψ → y = x
12 biimt ⊢ x ∈ A → φ ↔ x ∈ A → φ
13 df-ral ⊢ ∀ y ∈ A y = x → ψ ↔ ∀ y y ∈ A → y = x → ψ
14 bi2.04 ⊢ y ∈ A → y = x → ψ ↔ y = x → y ∈ A → ψ
15 14 albii ⊢ ∀ y y ∈ A → y = x → ψ ↔ ∀ y y = x → y ∈ A → ψ
16 eleq1w ⊢ x = y → x ∈ A ↔ y ∈ A
17 16 1 imbi12d ⊢ x = y → x ∈ A → φ ↔ y ∈ A → ψ
18 17 bicomd ⊢ x = y → y ∈ A → ψ ↔ x ∈ A → φ
19 18 equcoms ⊢ y = x → y ∈ A → ψ ↔ x ∈ A → φ
20 19 equsalvw ⊢ ∀ y y = x → y ∈ A → ψ ↔ x ∈ A → φ
21 13 15 20 3bitrri ⊢ x ∈ A → φ ↔ ∀ y ∈ A y = x → ψ
22 12 21 bitrdi ⊢ x ∈ A → φ ↔ ∀ y ∈ A y = x → ψ
23 11 22 anbi12d ⊢ x ∈ A → ∀ y ∈ A ψ → x = y ∧ φ ↔ ∀ y ∈ A ψ → y = x ∧ ∀ y ∈ A y = x → ψ
24 7 23 syl5bb ⊢ x ∈ A → φ ∧ ∀ y ∈ A ψ → x = y ↔ ∀ y ∈ A ψ → y = x ∧ ∀ y ∈ A y = x → ψ
25 6 24 bitr4id ⊢ 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