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
|- F/ x ph
Assertion r19.3rz
|- ( A =/= (/) -> ( ph <-> A. x e. A ph ) )

Proof

Step Hyp Ref Expression
1 r19.3rz.1
 |-  F/ x ph
2 n0
 |-  ( A =/= (/) <-> E. x x e. A )
3 biimt
 |-  ( E. x x e. A -> ( ph <-> ( E. x x e. A -> ph ) ) )
4 2 3 sylbi
 |-  ( A =/= (/) -> ( ph <-> ( E. x x e. A -> ph ) ) )
5 df-ral
 |-  ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
6 1 19.23
 |-  ( A. x ( x e. A -> ph ) <-> ( E. x x e. A -> ph ) )
7 5 6 bitri
 |-  ( A. x e. A ph <-> ( E. x x e. A -> ph ) )
8 4 7 bitr4di
 |-  ( A =/= (/) -> ( ph <-> A. x e. A ph ) )