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

Metamath Proof Explorer

Theorem rspcime

Description: Prove a restricted existential. (Contributed by Rohan Ridenour, 3-Aug-2023)

Ref Expression
Hypotheses rspcime.1 ⊢ φ ∧ x = A → ψ
rspcime.2 ⊢ φ → A ∈ B
Assertion rspcime ⊢ φ → ∃ x ∈ B ψ

Proof

Step Hyp Ref Expression
1 rspcime.1 ⊢ φ ∧ x = A → ψ
2 rspcime.2 ⊢ φ → A ∈ B
3 simpl ⊢ φ ∧ x = A → φ
4 1 3 2thd ⊢ φ ∧ x = A → ψ ↔ φ
5 id ⊢ φ → φ
6 2 4 5 rspcedvd ⊢ φ → ∃ x ∈ B ψ