Metamath Proof Explorer

Theorem r19.3rzv

Description: Restricted quantification of wff not containing quantified variable. (Contributed by NM, 10-Mar-1997)

Ref Expression
Assertion r19.3rzv 
|- ( A =/= (/) -> ( ph <-> A. x e. A ph ) )

Proof

Step Hyp Ref Expression
1 nfv 
 |-  F/ x ph
2 1 r19.3rz 
 |-  ( A =/= (/) -> ( ph <-> A. x e. A ph ) )