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

Metamath Proof Explorer

Theorem reueq1f

Description: Equality theorem for restricted unique existential quantifier, with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by NM, 5-Apr-2004) (Revised by Andrew Salmon, 11-Jul-2011)

Ref Expression
Hypotheses rmoeq1f.1 ⊢ Ⅎ _ x A
rmoeq1f.2 ⊢ Ⅎ _ x B
Assertion reueq1f ⊢ A = B → ∃! x ∈ A φ ↔ ∃! x ∈ B φ

Proof

Step Hyp Ref Expression
1 rmoeq1f.1 ⊢ Ⅎ _ x A
2 rmoeq1f.2 ⊢ Ⅎ _ x B
3 1 2 rexeqf ⊢ A = B → ∃ x ∈ A φ ↔ ∃ x ∈ B φ
4 1 2 rmoeq1f ⊢ A = B → ∃* x ∈ A φ ↔ ∃* x ∈ B φ
5 3 4 anbi12d ⊢ A = B → ∃ x ∈ A φ ∧ ∃* x ∈ A φ ↔ ∃ x ∈ B φ ∧ ∃* x ∈ B φ
6 reu5 ⊢ ∃! x ∈ A φ ↔ ∃ x ∈ A φ ∧ ∃* x ∈ A φ
7 reu5 ⊢ ∃! x ∈ B φ ↔ ∃ x ∈ B φ ∧ ∃* x ∈ B φ
8 5 6 7 3bitr4g ⊢ A = B → ∃! x ∈ A φ ↔ ∃! x ∈ B φ