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	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ∃! 𝑦 ∈ 𝐶 𝑥 = 𝐴 )