Metamath Proof Explorer

Theorem reuhypd

Description: A theorem useful for eliminating the restricted existential uniqueness hypotheses in riotaxfrd . (Contributed by NM, 16-Jan-2012)

Ref Expression
Hypotheses reuhypd.1 ⊢ φ ∧ x ∈ C → B ∈ C
reuhypd.2 ⊢ φ ∧ x ∈ C ∧ y ∈ C → x = A ↔ y = B
Assertion reuhypd ⊢ φ ∧ x ∈ C → ∃! y ∈ C x = A

Proof

Step Hyp Ref Expression
1 reuhypd.1 ⊢ φ ∧ x ∈ C → B ∈ C
2 reuhypd.2 ⊢ φ ∧ x ∈ C ∧ y ∈ C → x = A ↔ y = B
3 1 elexd ⊢ φ ∧ x ∈ C → B ∈ V
4 eueq ⊢ B ∈ V ↔ ∃! y y = B
5 3 4 sylib ⊢ φ ∧ x ∈ C → ∃! y y = B
6 eleq1 ⊢ y = B → y ∈ C ↔ B ∈ C
7 1 6 syl5ibrcom ⊢ φ ∧ x ∈ C → y = B → y ∈ C
8 7 pm4.71rd ⊢ φ ∧ x ∈ C → y = B ↔ y ∈ C ∧ y = B
9 2 3expa ⊢ φ ∧ x ∈ C ∧ y ∈ C → x = A ↔ y = B
10 9 pm5.32da ⊢ φ ∧ x ∈ C → y ∈ C ∧ x = A ↔ y ∈ C ∧ y = B
11 8 10 bitr4d ⊢ φ ∧ x ∈ C → y = B ↔ y ∈ C ∧ x = A
12 11 eubidv ⊢ φ ∧ x ∈ C → ∃! y y = B ↔ ∃! y y ∈ C ∧ x = A
13 5 12 mpbid ⊢ φ ∧ x ∈ C → ∃! y y ∈ C ∧ x = A
14 df-reu ⊢ ∃! y ∈ C x = A ↔ ∃! y y ∈ C ∧ x = A
15 13 14 sylibr ⊢ φ ∧ x ∈ C → ∃! y ∈ C x = A