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

Metamath Proof Explorer

Theorem rmoeqd

Description: Equality deduction for restricted at-most-one quantifier. (Contributed by Alexander van der Vekens, 17-Jun-2017)

Ref Expression
Hypothesis rmoeqd.1 ⊢ A = B → φ ↔ ψ
Assertion rmoeqd ⊢ A = B → ∃* x ∈ A φ ↔ ∃* x ∈ B ψ

Proof

Step Hyp Ref Expression
1 rmoeqd.1 ⊢ A = B → φ ↔ ψ
2 rmoeq1 ⊢ A = B → ∃* x ∈ A φ ↔ ∃* x ∈ B φ
3 1 rmobidv ⊢ A = B → ∃* x ∈ B φ ↔ ∃* x ∈ B ψ
4 2 3 bitrd ⊢ A = B → ∃* x ∈ A φ ↔ ∃* x ∈ B ψ