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

Metamath Proof Explorer

Theorem rexeqfOLD

Description: Obsolete version of rexeqf as of 9-Mar-2025. (Contributed by NM, 9-Oct-2003) (Revised by Andrew Salmon, 11-Jul-2011) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 raleqf.1 ⊢ Ⅎ _ x A
2 raleqf.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 exbid ⊢ A = B → ∃ x x ∈ A ∧ φ ↔ ∃ x x ∈ B ∧ φ
7 df-rex ⊢ ∃ x ∈ A φ ↔ ∃ x x ∈ A ∧ φ
8 df-rex ⊢ ∃ x ∈ B φ ↔ ∃ x x ∈ B ∧ φ
9 6 7 8 3bitr4g ⊢ A = B → ∃ x ∈ A φ ↔ ∃ x ∈ B φ