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

Metamath Proof Explorer

Theorem elabreximdv

Description: Class substitution in an image set. (Contributed by Thierry Arnoux, 30-Dec-2016)

Ref Expression
Hypotheses elabreximdv.1 ⊢ A = B → χ ↔ ψ
elabreximdv.2 ⊢ φ → A ∈ V
elabreximdv.3 ⊢ φ ∧ x ∈ C → ψ
Assertion elabreximdv ⊢ φ ∧ A ∈ y | ∃ x ∈ C y = B → χ

Proof

Step Hyp Ref Expression
1 elabreximdv.1 ⊢ A = B → χ ↔ ψ
2 elabreximdv.2 ⊢ φ → A ∈ V
3 elabreximdv.3 ⊢ φ ∧ x ∈ C → ψ
4 nfv ⊢ Ⅎ x φ
5 nfv ⊢ Ⅎ x χ
6 4 5 1 2 3 elabreximd ⊢ φ ∧ A ∈ y | ∃ x ∈ C y = B → χ