Theorem reusv3i

Description: Two ways of expressing existential uniqueness via an indirect equality. (Contributed by NM, 23-Dec-2012)

	Ref	Expression
Hypotheses	reusv3.1	⊢ ( 𝑦 = 𝑧 → ( 𝜑 ↔ 𝜓 ) )
	reusv3.2	⊢ ( 𝑦 = 𝑧 → 𝐶 = 𝐷 )
Assertion	reusv3i	⊢ ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) → ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝜑 ∧ 𝜓 ) → 𝐶 = 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		reusv3.1	⊢ ( 𝑦 = 𝑧 → ( 𝜑 ↔ 𝜓 ) )
2		reusv3.2	⊢ ( 𝑦 = 𝑧 → 𝐶 = 𝐷 )
3	2	eqeq2d	⊢ ( 𝑦 = 𝑧 → ( 𝑥 = 𝐶 ↔ 𝑥 = 𝐷 ) )
4	1 3	imbi12d	⊢ ( 𝑦 = 𝑧 → ( ( 𝜑 → 𝑥 = 𝐶 ) ↔ ( 𝜓 → 𝑥 = 𝐷 ) ) )
5	4	cbvralvw	⊢ ( ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) ↔ ∀ 𝑧 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐷 ) )
6	5	biimpi	⊢ ( ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) → ∀ 𝑧 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐷 ) )
7		raaanv	⊢ ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝜑 → 𝑥 = 𝐶 ) ∧ ( 𝜓 → 𝑥 = 𝐷 ) ) ↔ ( ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) ∧ ∀ 𝑧 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐷 ) ) )
8		anim12	⊢ ( ( ( 𝜑 → 𝑥 = 𝐶 ) ∧ ( 𝜓 → 𝑥 = 𝐷 ) ) → ( ( 𝜑 ∧ 𝜓 ) → ( 𝑥 = 𝐶 ∧ 𝑥 = 𝐷 ) ) )
9		eqtr2	⊢ ( ( 𝑥 = 𝐶 ∧ 𝑥 = 𝐷 ) → 𝐶 = 𝐷 )
10	8 9	syl6	⊢ ( ( ( 𝜑 → 𝑥 = 𝐶 ) ∧ ( 𝜓 → 𝑥 = 𝐷 ) ) → ( ( 𝜑 ∧ 𝜓 ) → 𝐶 = 𝐷 ) )
11	10	2ralimi	⊢ ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝜑 → 𝑥 = 𝐶 ) ∧ ( 𝜓 → 𝑥 = 𝐷 ) ) → ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝜑 ∧ 𝜓 ) → 𝐶 = 𝐷 ) )
12	7 11	sylbir	⊢ ( ( ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) ∧ ∀ 𝑧 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐷 ) ) → ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝜑 ∧ 𝜓 ) → 𝐶 = 𝐷 ) )
13	6 12	mpdan	⊢ ( ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) → ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝜑 ∧ 𝜓 ) → 𝐶 = 𝐷 ) )
14	13	rexlimivw	⊢ ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) → ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝜑 ∧ 𝜓 ) → 𝐶 = 𝐷 ) )