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	⊢ ( Ⅎ 𝑥 ∈ 𝐴 𝜑 ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 → ∀ 𝑥 ∈ 𝐴 𝜑 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	⊢ 𝑥
1		cA	⊢ 𝐴
2		wph	⊢ 𝜑
3	2 0 1	wrnf	⊢ Ⅎ 𝑥 ∈ 𝐴 𝜑
4	2 0 1	wrex	⊢ ∃ 𝑥 ∈ 𝐴 𝜑
5	2 0 1	wral	⊢ ∀ 𝑥 ∈ 𝐴 𝜑
6	4 5	wi	⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 → ∀ 𝑥 ∈ 𝐴 𝜑 )
7	3 6	wb	⊢ ( Ⅎ 𝑥 ∈ 𝐴 𝜑 ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 → ∀ 𝑥 ∈ 𝐴 𝜑 ) )