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 x A y A φ x A φ


Step Hyp Ref Expression
1 biidd y = x φ φ
2 1 rspcv x A y A φ φ
3 2 ralimia x A y A φ x A φ
4 ax-1 φ y A φ
5 4 ralrimiv φ y A φ
6 5 ralimi x A φ x A y A φ
7 3 6 impbii x A y A φ x A φ