Metamath Proof Explorer


Theorem rr19.3v

Description: Restricted quantifier version of Theorem 19.3 of Margaris p. 89. We don't need the nonempty class condition of r19.3rzv when there is an outer quantifier. (Contributed by NM, 25-Oct-2012)

Ref Expression
Assertion rr19.3v
|- ( A. x e. A A. y e. A ph <-> A. x e. A ph )

Proof

Step Hyp Ref Expression
1 biidd
 |-  ( y = x -> ( ph <-> ph ) )
2 1 rspcv
 |-  ( x e. A -> ( A. y e. A ph -> ph ) )
3 2 ralimia
 |-  ( A. x e. A A. y e. A ph -> A. x e. A ph )
4 ax-1
 |-  ( ph -> ( y e. A -> ph ) )
5 4 ralrimiv
 |-  ( ph -> A. y e. A ph )
6 5 ralimi
 |-  ( A. x e. A ph -> A. x e. A A. y e. A ph )
7 3 6 impbii
 |-  ( A. x e. A A. y e. A ph <-> A. x e. A ph )