Metamath Proof Explorer

Theorem reu7

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

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

Proof

Step Hyp Ref Expression
1 rmo4.1 ⊢ x = y → φ ↔ ψ
2 reu3 ⊢ ∃! x ∈ A φ ↔ ∃ x ∈ A φ ∧ ∃ z ∈ A ∀ x ∈ A φ → x = z
3 equequ1 ⊢ x = y → x = z ↔ y = z
4 equcom ⊢ y = z ↔ z = y
5 3 4 bitrdi ⊢ x = y → x = z ↔ z = y
6 1 5 imbi12d ⊢ x = y → φ → x = z ↔ ψ → z = y
7 6 cbvralvw ⊢ ∀ x ∈ A φ → x = z ↔ ∀ y ∈ A ψ → z = y
8 7 rexbii ⊢ ∃ z ∈ A ∀ x ∈ A φ → x = z ↔ ∃ z ∈ A ∀ y ∈ A ψ → z = y
9 equequ1 ⊢ z = x → z = y ↔ x = y
10 9 imbi2d ⊢ z = x → ψ → z = y ↔ ψ → x = y
11 10 ralbidv ⊢ z = x → ∀ y ∈ A ψ → z = y ↔ ∀ y ∈ A ψ → x = y
12 11 cbvrexvw ⊢ ∃ z ∈ A ∀ y ∈ A ψ → z = y ↔ ∃ x ∈ A ∀ y ∈ A ψ → x = y
13 8 12 bitri ⊢ ∃ z ∈ A ∀ x ∈ A φ → x = z ↔ ∃ x ∈ A ∀ y ∈ A ψ → x = y
14 13 anbi2i ⊢ ∃ x ∈ A φ ∧ ∃ z ∈ A ∀ x ∈ A φ → x = z ↔ ∃ x ∈ A φ ∧ ∃ x ∈ A ∀ y ∈ A ψ → x = y
15 2 14 bitri ⊢ ∃! x ∈ A φ ↔ ∃ x ∈ A φ ∧ ∃ x ∈ A ∀ y ∈ A ψ → x = y