Definition df-bj-rnf

Description: Definition of restricted nonfreeness. Informally, the proposition F/ x e. A ph means that ph ( x ) does not vary on A . (Contributed by BJ, 19-Mar-2021)

	Ref	Expression
Assertion	df-bj-rnf	|- ( F/ x e. A ph <-> ( E. x e. A ph -> A. x e. A ph ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	|- x
1		cA	|- A
2		wph	|- ph
3	2 0 1	wrnf	|- F/ x e. A ph
4	2 0 1	wrex	|- E. x e. A ph
5	2 0 1	wral	|- A. x e. A ph
6	4 5	wi	|- ( E. x e. A ph -> A. x e. A ph )
7	3 6	wb	|- ( F/ x e. A ph <-> ( E. x e. A ph -> A. x e. A ph ) )