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

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 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐵 ∈ 𝐶 )
reuhypd.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) → ( 𝑥 = 𝐴 ↔ 𝑦 = 𝐵 ) )
Assertion reuhypd ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ∃! 𝑦 ∈ 𝐶 𝑥 = 𝐴 )

Proof

Step Hyp Ref Expression
1 reuhypd.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐵 ∈ 𝐶 )
2 reuhypd.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) → ( 𝑥 = 𝐴 ↔ 𝑦 = 𝐵 ) )
3 1 elexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐵 ∈ V )
4 eueq ⊢ ( 𝐵 ∈ V ↔ ∃! 𝑦 𝑦 = 𝐵 )
5 3 4 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ∃! 𝑦 𝑦 = 𝐵 )
6 eleq1 ⊢ ( 𝑦 = 𝐵 → ( 𝑦 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶 ) )
7 1 6 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( 𝑦 = 𝐵 → 𝑦 ∈ 𝐶 ) )
8 7 pm4.71rd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( 𝑦 = 𝐵 ↔ ( 𝑦 ∈ 𝐶 ∧ 𝑦 = 𝐵 ) ) )
9 2 3expa ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐶 ) → ( 𝑥 = 𝐴 ↔ 𝑦 = 𝐵 ) )
10 9 pm5.32da ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( 𝑦 ∈ 𝐶 ∧ 𝑥 = 𝐴 ) ↔ ( 𝑦 ∈ 𝐶 ∧ 𝑦 = 𝐵 ) ) )
11 8 10 bitr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( 𝑦 = 𝐵 ↔ ( 𝑦 ∈ 𝐶 ∧ 𝑥 = 𝐴 ) ) )
12 11 eubidv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ∃! 𝑦 𝑦 = 𝐵 ↔ ∃! 𝑦 ( 𝑦 ∈ 𝐶 ∧ 𝑥 = 𝐴 ) ) )
13 5 12 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ∃! 𝑦 ( 𝑦 ∈ 𝐶 ∧ 𝑥 = 𝐴 ) )
14 df-reu ⊢ ( ∃! 𝑦 ∈ 𝐶 𝑥 = 𝐴 ↔ ∃! 𝑦 ( 𝑦 ∈ 𝐶 ∧ 𝑥 = 𝐴 ) )
15 13 14 sylibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ∃! 𝑦 ∈ 𝐶 𝑥 = 𝐴 )