Metamath Proof Explorer

Theorem r19.40

Description: Restricted quantifier version of Theorem 19.40 of Margaris p. 90. (Contributed by NM, 2-Apr-2004)

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

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( ph /\ ps ) -> ph )
2 1 reximi 
 |-  ( E. x e. A ( ph /\ ps ) -> E. x e. A ph )
3 simpr 
 |-  ( ( ph /\ ps ) -> ps )
4 3 reximi 
 |-  ( E. x e. A ( ph /\ ps ) -> E. x e. A ps )
5 2 4 jca 
 |-  ( E. x e. A ( ph /\ ps ) -> ( E. x e. A ph /\ E. x e. A ps ) )