Definition df-nfOLD 1721

Description: Obsolete definition replaced by nf5 2116 as of 3-Oct-2021. This definition is less suitable than df-nf 1710 when ax-10 2019 and ax-12 2047 are not in effect. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.)

Assertion

Ref	Expression
df-nfOLD	⊢ (Ⅎ𝑥𝜑 ↔ ∀𝑥(𝜑 → ∀𝑥𝜑))

Detailed syntax breakdown of Definition df-nfOLD

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		vx	. . 3 setvar 𝑥
3	1, 2	wnfOLD 1709	. 2 wff Ⅎ𝑥𝜑
4	1, 2	wal 1481	. . . 4 wff ∀𝑥𝜑
5	1, 4	wi 4	. . 3 wff (𝜑 → ∀𝑥𝜑)
6	5, 2	wal 1481	. 2 wff ∀𝑥(𝜑 → ∀𝑥𝜑)
7	3, 6	wb 196	1 wff (Ⅎ𝑥𝜑 ↔ ∀𝑥(𝜑 → ∀𝑥𝜑))

This definition is referenced by:  nfiOLD  1734  nfbiiOLD  1836  nfdvOLD  1873  nfrOLD  2188  nfdOLD  2193  nfbidfOLD  2201  19.9dOLD  2203  nfnf1OLDOLD  2208  nfntOLD  2209  nfimdOLD  2226