Definition df-bj-rnf 35130

Description: Definition of restricted nonfreeness. Informally, the proposition Ⅎ𝑥 ∈ 𝐴𝜑 means that 𝜑(𝑥) does not vary on 𝐴. (Contributed by BJ, 19-Mar-2021.)

Assertion

Ref	Expression
df-bj-rnf	⊢ (Ⅎ𝑥 ∈ 𝐴𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜑))

Detailed syntax breakdown of Definition df-bj-rnf

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		vx	. . 3 setvar 𝑥
3		cA	. . 3 class 𝐴
4	1, 2, 3	wrnf 35129	. 2 wff Ⅎ𝑥 ∈ 𝐴𝜑
5	1, 2, 3	wrex 3065	. . 3 wff ∃𝑥 ∈ 𝐴 𝜑
6	1, 2, 3	wral 3064	. . 3 wff ∀𝑥 ∈ 𝐴 𝜑
7	5, 6	wi 4	. 2 wff (∃𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜑)
8	4, 7	wb 205	1 wff (Ⅎ𝑥 ∈ 𝐴𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜑))

This definition is referenced by: (None)