Theorem rspc2ev

Description: 2-variable restricted existential specialization, using implicit substitution. (Contributed by NM, 16-Oct-1999)

	Ref	Expression
Hypotheses	rspc2v.1	|- ( x = A -> ( ph <-> ch ) )
	rspc2v.2	|- ( y = B -> ( ch <-> ps ) )
Assertion	rspc2ev	|- ( ( A e. C /\ B e. D /\ ps ) -> E. x e. C E. y e. D ph )

Proof

Step	Hyp	Ref	Expression
1		rspc2v.1	|- ( x = A -> ( ph <-> ch ) )
2		rspc2v.2	|- ( y = B -> ( ch <-> ps ) )
3	2	rspcev	|- ( ( B e. D /\ ps ) -> E. y e. D ch )
4	3	anim2i	|- ( ( A e. C /\ ( B e. D /\ ps ) ) -> ( A e. C /\ E. y e. D ch ) )
5	4	3impb	|- ( ( A e. C /\ B e. D /\ ps ) -> ( A e. C /\ E. y e. D ch ) )
6	1	rexbidv	|- ( x = A -> ( E. y e. D ph <-> E. y e. D ch ) )
7	6	rspcev	|- ( ( A e. C /\ E. y e. D ch ) -> E. x e. C E. y e. D ph )
8	5 7	syl	|- ( ( A e. C /\ B e. D /\ ps ) -> E. x e. C E. y e. D ph )