Theorem rspe

Description: Restricted specialization. (Contributed by NM, 12-Oct-1999)

	Ref	Expression
Assertion	rspe	|- ( ( x e. A /\ ph ) -> E. x e. A ph )

Proof

Step	Hyp	Ref	Expression
1		19.8a	|- ( ( x e. A /\ ph ) -> E. x ( x e. A /\ ph ) )
2		df-rex	|- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
3	1 2	sylibr	|- ( ( x e. A /\ ph ) -> E. x e. A ph )