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

Metamath Proof Explorer

Theorem rr19.28v

Description: Restricted quantifier version of Theorem 19.28 of Margaris p. 90. We don't need the nonempty class condition of r19.28zv when there is an outer quantifier. (Contributed by NM, 29-Oct-2012)

Ref Expression
Assertion rr19.28v 
|- ( A. x e. A A. y e. A ( ph /\ ps ) <-> A. x e. A ( ph /\ A. y e. A ps ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( ph /\ ps ) -> ph )
2 1 ralimi 
 |-  ( A. y e. A ( ph /\ ps ) -> A. y e. A ph )
3 biidd 
 |-  ( y = x -> ( ph <-> ph ) )
4 3 rspcv 
 |-  ( x e. A -> ( A. y e. A ph -> ph ) )
5 2 4 syl5 
 |-  ( x e. A -> ( A. y e. A ( ph /\ ps ) -> ph ) )
6 simpr 
 |-  ( ( ph /\ ps ) -> ps )
7 6 ralimi 
 |-  ( A. y e. A ( ph /\ ps ) -> A. y e. A ps )
8 5 7 jca2 
 |-  ( x e. A -> ( A. y e. A ( ph /\ ps ) -> ( ph /\ A. y e. A ps ) ) )
9 8 ralimia 
 |-  ( A. x e. A A. y e. A ( ph /\ ps ) -> A. x e. A ( ph /\ A. y e. A ps ) )
10 r19.28v 
 |-  ( ( ph /\ A. y e. A ps ) -> A. y e. A ( ph /\ ps ) )
11 10 ralimi 
 |-  ( A. x e. A ( ph /\ A. y e. A ps ) -> A. x e. A A. y e. A ( ph /\ ps ) )
12 9 11 impbii 
 |-  ( A. x e. A A. y e. A ( ph /\ ps ) <-> A. x e. A ( ph /\ A. y e. A ps ) )