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	$$⊢Ⅎx\in A\phi \leftrightarrow \left(\exists x\in A\phi \to \forall x\in A\phi \right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$$setvarx$$
1		cA	$$classA$$
2		wph	$$wff\phi$$
3	2 0 1	wrnf	$$wffℲx\in A\phi$$
4	2 0 1	wrex	$$wff\exists x\in A\phi$$
5	2 0 1	wral	$$wff\forall x\in A\phi$$
6	4 5	wi	$$wff\left(\exists x\in A\phi \to \forall x\in A\phi \right)$$
7	3 6	wb	$$wff\left(Ⅎx\in A\phi \leftrightarrow \left(\exists x\in A\phi \to \forall x\in A\phi \right)\right)$$