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

Metamath Proof Explorer

Theorem reuxfr1d

Description: Transfer existential uniqueness from a variable x to another variable y contained in expression A . Cf. reuxfr1ds . (Contributed by Thierry Arnoux, 7-Apr-2017)

Ref Expression
Hypotheses reuxfr1d.1 ⊢ φ ∧ y ∈ C → A ∈ B
reuxfr1d.2 ⊢ φ ∧ x ∈ B → ∃! y ∈ C x = A
reuxfr1d.3 ⊢ φ ∧ x = A → ψ ↔ χ
Assertion reuxfr1d ⊢ φ → ∃! x ∈ B ψ ↔ ∃! y ∈ C χ

Proof

Step Hyp Ref Expression
1 reuxfr1d.1 ⊢ φ ∧ y ∈ C → A ∈ B
2 reuxfr1d.2 ⊢ φ ∧ x ∈ B → ∃! y ∈ C x = A
3 reuxfr1d.3 ⊢ φ ∧ x = A → ψ ↔ χ
4 reurex ⊢ ∃! y ∈ C x = A → ∃ y ∈ C x = A
5 2 4 syl ⊢ φ ∧ x ∈ B → ∃ y ∈ C x = A
6 5 biantrurd ⊢ φ ∧ x ∈ B → ψ ↔ ∃ y ∈ C x = A ∧ ψ
7 r19.41v ⊢ ∃ y ∈ C x = A ∧ ψ ↔ ∃ y ∈ C x = A ∧ ψ
8 3 pm5.32da ⊢ φ → x = A ∧ ψ ↔ x = A ∧ χ
9 8 rexbidv ⊢ φ → ∃ y ∈ C x = A ∧ ψ ↔ ∃ y ∈ C x = A ∧ χ
10 7 9 bitr3id ⊢ φ → ∃ y ∈ C x = A ∧ ψ ↔ ∃ y ∈ C x = A ∧ χ
11 10 adantr ⊢ φ ∧ x ∈ B → ∃ y ∈ C x = A ∧ ψ ↔ ∃ y ∈ C x = A ∧ χ
12 6 11 bitrd ⊢ φ ∧ x ∈ B → ψ ↔ ∃ y ∈ C x = A ∧ χ
13 12 reubidva ⊢ φ → ∃! x ∈ B ψ ↔ ∃! x ∈ B ∃ y ∈ C x = A ∧ χ
14 reurmo ⊢ ∃! y ∈ C x = A → ∃* y ∈ C x = A
15 2 14 syl ⊢ φ ∧ x ∈ B → ∃* y ∈ C x = A
16 1 15 reuxfrd ⊢ φ → ∃! x ∈ B ∃ y ∈ C x = A ∧ χ ↔ ∃! y ∈ C χ
17 13 16 bitrd ⊢ φ → ∃! x ∈ B ψ ↔ ∃! y ∈ C χ