Theorem rr-spce

Description: Prove an existential. (Contributed by Rohan Ridenour, 12-Aug-2023)

	Ref	Expression
Hypotheses	rr-spce.1	|- ( ( ph /\ x = A ) -> ps )
	rr-spce.2	|- ( ph -> A e. V )
Assertion	rr-spce	|- ( ph -> E. x ps )

Proof

Step	Hyp	Ref	Expression
1		rr-spce.1	|- ( ( ph /\ x = A ) -> ps )
2		rr-spce.2	|- ( ph -> A e. V )
3	2	elexd	|- ( ph -> A e. _V )
4		isset	|- ( A e. _V <-> E. x x = A )
5	3 4	sylib	|- ( ph -> E. x x = A )
6	1	ex	|- ( ph -> ( x = A -> ps ) )
7	6	eximdv	|- ( ph -> ( E. x x = A -> E. x ps ) )
8	5 7	mpd	|- ( ph -> E. x ps )