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

Metamath Proof Explorer

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 ⊢ ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) → ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝜑 ∧ 𝜓 ) → 𝐶 = 𝐷 ) )