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

Metamath Proof Explorer

Theorem rmoeq1f

Description: Equality theorem for restricted at-most-one quantifier, with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by Alexander van der Vekens, 17-Jun-2017)

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

Proof

Step Hyp Ref Expression
1 rmoeq1f.1 ⊢ Ⅎ _ x A
2 rmoeq1f.2 ⊢ Ⅎ _ x B
3 1 2 nfeq ⊢ Ⅎ x A = B
4 eleq2 ⊢ A = B → x ∈ A ↔ x ∈ B
5 4 anbi1d ⊢ A = B → x ∈ A ∧ φ ↔ x ∈ B ∧ φ
6 3 5 mobid ⊢ A = B → ∃* x x ∈ A ∧ φ ↔ ∃* x x ∈ B ∧ φ
7 df-rmo ⊢ ∃* x ∈ A φ ↔ ∃* x x ∈ A ∧ φ
8 df-rmo ⊢ ∃* x ∈ B φ ↔ ∃* x x ∈ B ∧ φ
9 6 7 8 3bitr4g ⊢ A = B → ∃* x ∈ A φ ↔ ∃* x ∈ B φ