Metamath Proof Explorer


Theorem rspcef

Description: Restricted existential specialization, using implicit substitution. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses rspcef.1 𝑥 𝜓
rspcef.2 𝑥 𝐴
rspcef.3 𝑥 𝐵
rspcef.4 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) )
Assertion rspcef ( ( 𝐴𝐵𝜓 ) → ∃ 𝑥𝐵 𝜑 )

Proof

Step Hyp Ref Expression
1 rspcef.1 𝑥 𝜓
2 rspcef.2 𝑥 𝐴
3 rspcef.3 𝑥 𝐵
4 rspcef.4 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) )
5 1 2 3 4 rspcegf ( ( 𝐴𝐵𝜓 ) → ∃ 𝑥𝐵 𝜑 )