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

Metamath Proof Explorer

Theorem reu2eqd

Description: Deduce equality from restricted uniqueness, deduction version. (Contributed by Thierry Arnoux, 27-Nov-2019)

Ref Expression
Hypotheses reu2eqd.1 ⊢ x = B → ψ ↔ χ
reu2eqd.2 ⊢ x = C → ψ ↔ θ
reu2eqd.3 ⊢ φ → ∃! x ∈ A ψ
reu2eqd.4 ⊢ φ → B ∈ A
reu2eqd.5 ⊢ φ → C ∈ A
reu2eqd.6 ⊢ φ → χ
reu2eqd.7 ⊢ φ → θ
Assertion reu2eqd ⊢ φ → B = C

Proof

Step Hyp Ref Expression
1 reu2eqd.1 ⊢ x = B → ψ ↔ χ
2 reu2eqd.2 ⊢ x = C → ψ ↔ θ
3 reu2eqd.3 ⊢ φ → ∃! x ∈ A ψ
4 reu2eqd.4 ⊢ φ → B ∈ A
5 reu2eqd.5 ⊢ φ → C ∈ A
6 reu2eqd.6 ⊢ φ → χ
7 reu2eqd.7 ⊢ φ → θ
8 reu2 ⊢ ∃! x ∈ A ψ ↔ ∃ x ∈ A ψ ∧ ∀ x ∈ A ∀ y ∈ A ψ ∧ y x ψ → x = y
9 3 8 sylib ⊢ φ → ∃ x ∈ A ψ ∧ ∀ x ∈ A ∀ y ∈ A ψ ∧ y x ψ → x = y
10 9 simprd ⊢ φ → ∀ x ∈ A ∀ y ∈ A ψ ∧ y x ψ → x = y
11 nfv ⊢ Ⅎ x χ
12 nfs1v ⊢ Ⅎ x y x ψ
13 11 12 nfan ⊢ Ⅎ x χ ∧ y x ψ
14 nfv ⊢ Ⅎ x B = y
15 13 14 nfim ⊢ Ⅎ x χ ∧ y x ψ → B = y
16 nfv ⊢ Ⅎ y χ ∧ θ → B = C
17 1 anbi1d ⊢ x = B → ψ ∧ y x ψ ↔ χ ∧ y x ψ
18 eqeq1 ⊢ x = B → x = y ↔ B = y
19 17 18 imbi12d ⊢ x = B → ψ ∧ y x ψ → x = y ↔ χ ∧ y x ψ → B = y
20 nfv ⊢ Ⅎ x θ
21 20 2 sbhypf ⊢ y = C → y x ψ ↔ θ
22 21 anbi2d ⊢ y = C → χ ∧ y x ψ ↔ χ ∧ θ
23 eqeq2 ⊢ y = C → B = y ↔ B = C
24 22 23 imbi12d ⊢ y = C → χ ∧ y x ψ → B = y ↔ χ ∧ θ → B = C
25 15 16 19 24 rspc2 ⊢ B ∈ A ∧ C ∈ A → ∀ x ∈ A ∀ y ∈ A ψ ∧ y x ψ → x = y → χ ∧ θ → B = C
26 4 5 25 syl2anc ⊢ φ → ∀ x ∈ A ∀ y ∈ A ψ ∧ y x ψ → x = y → χ ∧ θ → B = C
27 10 26 mpd ⊢ φ → χ ∧ θ → B = C
28 6 7 27 mp2and ⊢ φ → B = C