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

Metamath Proof Explorer

Theorem rmoeq1

Description: Equality theorem for restricted at-most-one quantifier. (Contributed by Alexander van der Vekens, 17-Jun-2017) Remove usage of ax-10 , ax-11 , and ax-12 . (Revised by Steven Nguyen, 30-Apr-2023) Avoid ax-8 . (Revised by Wolf Lammen, 12-Mar-2025)

Ref Expression
Assertion rmoeq1 ⊢ A = B → ∃* x ∈ A φ ↔ ∃* x ∈ B φ

Proof

Step Hyp Ref Expression
1 dfcleq ⊢ A = B ↔ ∀ x x ∈ A ↔ x ∈ B
2 1 biimpi ⊢ A = B → ∀ x x ∈ A ↔ x ∈ B
3 anbi1 ⊢ x ∈ A ↔ x ∈ B → x ∈ A ∧ φ ↔ x ∈ B ∧ φ
4 3 imbi1d ⊢ x ∈ A ↔ x ∈ B → x ∈ A ∧ φ → x = z ↔ x ∈ B ∧ φ → x = z
5 4 alimi ⊢ ∀ x x ∈ A ↔ x ∈ B → ∀ x x ∈ A ∧ φ → x = z ↔ x ∈ B ∧ φ → x = z
6 albi ⊢ ∀ x x ∈ A ∧ φ → x = z ↔ x ∈ B ∧ φ → x = z → ∀ x x ∈ A ∧ φ → x = z ↔ ∀ x x ∈ B ∧ φ → x = z
7 2 5 6 3syl ⊢ A = B → ∀ x x ∈ A ∧ φ → x = z ↔ ∀ x x ∈ B ∧ φ → x = z
8 7 exbidv ⊢ A = B → ∃ z ∀ x x ∈ A ∧ φ → x = z ↔ ∃ z ∀ x x ∈ B ∧ φ → x = z
9 df-mo ⊢ ∃* x x ∈ A ∧ φ ↔ ∃ z ∀ x x ∈ A ∧ φ → x = z
10 df-mo ⊢ ∃* x x ∈ B ∧ φ ↔ ∃ z ∀ x x ∈ B ∧ φ → x = z
11 8 9 10 3bitr4g ⊢ A = B → ∃* x x ∈ A ∧ φ ↔ ∃* x x ∈ B ∧ φ
12 df-rmo ⊢ ∃* x ∈ A φ ↔ ∃* x x ∈ A ∧ φ
13 df-rmo ⊢ ∃* x ∈ B φ ↔ ∃* x x ∈ B ∧ φ
14 11 12 13 3bitr4g ⊢ A = B → ∃* x ∈ A φ ↔ ∃* x ∈ B φ