Metamath Proof Explorer


Theorem r19.3rz

Description: Restricted quantification of wff not containing quantified variable. (Contributed by FL, 3-Jan-2008)

Ref Expression
Hypothesis r19.3rz.1 x φ
Assertion r19.3rz A φ x A φ

Proof

Step Hyp Ref Expression
1 r19.3rz.1 x φ
2 n0 A x x A
3 biimt x x A φ x x A φ
4 2 3 sylbi A φ x x A φ
5 df-ral x A φ x x A φ
6 1 19.23 x x A φ x x A φ
7 5 6 bitri x A φ x x A φ
8 4 7 bitr4di A φ x A φ