Theorem rspcevOLD

Description: Obsolete version of rspce as of 12-Dec-2023. Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	rspcv.1	|- ( x = A -> ( ph <-> ps ) )
Assertion	rspcevOLD	|- ( ( A e. B /\ ps ) -> E. x e. B ph )

Proof

Step	Hyp	Ref	Expression
1		rspcv.1	|- ( x = A -> ( ph <-> ps ) )
2		nfv	|- F/ x ps
3	2 1	rspce	|- ( ( A e. B /\ ps ) -> E. x e. B ph )