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