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