Definition df-bj-nf 31765

Description: Alternate definition of the "semantically non-free" predicate, equivalent to nf5 2102 by df-nf 1701. This definition is stricter than nf5 2102 as soon as one has sp 2041, and less strict as soon as one has ax-10 2006. This version has no nested quantifiers, so is easier to understand and easier to handle when ax-10 2006 is not yet available, as illustrated by the results below (see bj-nfbi 31793 bj-nfn 31795). (Contributed by BJ, 6-May-2019.)

Assertion

Ref	Expression
df-bj-nf	⊢ (ℲℲ𝑥𝜑 ↔ (∃𝑥𝜑 → ∀𝑥𝜑))

Detailed syntax breakdown of Definition df-bj-nf

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		vx	. . 3 setvar 𝑥
3	1, 2	wnff 31764	. 2 wff ℲℲ𝑥𝜑
4	1, 2	wex 1695	. . 3 wff ∃𝑥𝜑
5	1, 2	wal 1473	. . 3 wff ∀𝑥𝜑
6	4, 5	wi 4	. 2 wff (∃𝑥𝜑 → ∀𝑥𝜑)
7	3, 6	wb 195	1 wff (ℲℲ𝑥𝜑 ↔ (∃𝑥𝜑 → ∀𝑥𝜑))

This definition is referenced by:  bj-nf2  31766  bj-nftht  31769  bj-alrimhi  31789  bj-nfbi  31793  bj-nfv  31806  bj-ssbft  31831