This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )