Metamath Proof Explorer


Theorem rspcef

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

Ref Expression
Hypotheses rspcef.1 x ψ
rspcef.2 _ x A
rspcef.3 _ x B
rspcef.4 x = A φ ψ
Assertion rspcef A B ψ x B φ

Proof

Step Hyp Ref Expression
1 rspcef.1 x ψ
2 rspcef.2 _ x A
3 rspcef.3 _ x B
4 rspcef.4 x = A φ ψ
5 1 2 3 4 rspcegf A B ψ x B φ