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

Metamath Proof Explorer

Theorem rexeqbid

Description: Equality deduction for restricted existential quantifier. See rexeqbidv for a version based on fewer axioms. (Contributed by Thierry Arnoux, 8-Mar-2017)

Ref Expression
Hypotheses raleqbid.0 ⊢ Ⅎ x φ
raleqbid.1 ⊢ Ⅎ _ x A
raleqbid.2 ⊢ Ⅎ _ x B
raleqbid.3 ⊢ φ → A = B
raleqbid.4 ⊢ φ → ψ ↔ χ
Assertion rexeqbid ⊢ φ → ∃ x ∈ A ψ ↔ ∃ x ∈ B χ

Proof

Step Hyp Ref Expression
1 raleqbid.0 ⊢ Ⅎ x φ
2 raleqbid.1 ⊢ Ⅎ _ x A
3 raleqbid.2 ⊢ Ⅎ _ x B
4 raleqbid.3 ⊢ φ → A = B
5 raleqbid.4 ⊢ φ → ψ ↔ χ
6 2 3 rexeqf ⊢ A = B → ∃ x ∈ A ψ ↔ ∃ x ∈ B ψ
7 4 6 syl ⊢ φ → ∃ x ∈ A ψ ↔ ∃ x ∈ B ψ
8 1 5 rexbid ⊢ φ → ∃ x ∈ B ψ ↔ ∃ x ∈ B χ
9 7 8 bitrd ⊢ φ → ∃ x ∈ A ψ ↔ ∃ x ∈ B χ