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 ⊢ y = z → φ ↔ ψ
reusv3.2 ⊢ y = z → C = D
Assertion reusv3i ⊢ ∃ x ∈ A ∀ y ∈ B φ → x = C → ∀ y ∈ B ∀ z ∈ B φ ∧ ψ → C = D

Proof

Step Hyp Ref Expression
1 reusv3.1 ⊢ y = z → φ ↔ ψ
2 reusv3.2 ⊢ y = z → C = D
3 2 eqeq2d ⊢ y = z → x = C ↔ x = D
4 1 3 imbi12d ⊢ y = z → φ → x = C ↔ ψ → x = D
5 4 cbvralvw ⊢ ∀ y ∈ B φ → x = C ↔ ∀ z ∈ B ψ → x = D
6 5 biimpi ⊢ ∀ y ∈ B φ → x = C → ∀ z ∈ B ψ → x = D
7 raaanv ⊢ ∀ y ∈ B ∀ z ∈ B φ → x = C ∧ ψ → x = D ↔ ∀ y ∈ B φ → x = C ∧ ∀ z ∈ B ψ → x = D
8 anim12 ⊢ φ → x = C ∧ ψ → x = D → φ ∧ ψ → x = C ∧ x = D
9 eqtr2 ⊢ x = C ∧ x = D → C = D
10 8 9 syl6 ⊢ φ → x = C ∧ ψ → x = D → φ ∧ ψ → C = D
11 10 2ralimi ⊢ ∀ y ∈ B ∀ z ∈ B φ → x = C ∧ ψ → x = D → ∀ y ∈ B ∀ z ∈ B φ ∧ ψ → C = D
12 7 11 sylbir ⊢ ∀ y ∈ B φ → x = C ∧ ∀ z ∈ B ψ → x = D → ∀ y ∈ B ∀ z ∈ B φ ∧ ψ → C = D
13 6 12 mpdan ⊢ ∀ y ∈ B φ → x = C → ∀ y ∈ B ∀ z ∈ B φ ∧ ψ → C = D
14 13 rexlimivw ⊢ ∃ x ∈ A ∀ y ∈ B φ → x = C → ∀ y ∈ B ∀ z ∈ B φ ∧ ψ → C = D