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

Metamath Proof Explorer

Theorem r19.3rzf

Description: Restricted quantification of wff not containing quantified variable. (Contributed by Glauco Siliprandi, 24-Jan-2025)

Ref Expression
Hypotheses r19.3rzf.1 
|- F/ x ph
r19.3rzf.2 
|- F/_ x A
Assertion r19.3rzf 
|- ( A =/= (/) -> ( ph <-> A. x e. A ph ) )

Proof

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