This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )