Definition df-nfOLD 1712

Description: Obsolete definition replaced by nf5 2102 as of 3-Oct-2021. This definition is less suitable than df-nf 1701 when ax-10 2006 and ax-12 2034 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 1700	. 2 wff Ⅎ𝑥𝜑
4	1, 2	wal 1473	. . . 4 wff ∀𝑥𝜑
5	1, 4	wi 4	. . 3 wff (𝜑 → ∀𝑥𝜑)
6	5, 2	wal 1473	. 2 wff ∀𝑥(𝜑 → ∀𝑥𝜑)
7	3, 6	wb 195	1 wff (Ⅎ𝑥𝜑 ↔ ∀𝑥(𝜑 → ∀𝑥𝜑))

This definition is referenced by:  nfiOLD  1725  nfbiiOLD  1824  nfdvOLD  1860  nfrOLD  2176  nfdOLD  2181  nfbidfOLD  2189  19.9dOLD  2191  nfnf1OLDOLD  2196  nfntOLD  2197  nfimdOLD  2214