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	|- ( F/ x ph <-> A. x ( ph -> A. x ph ) )

Detailed syntax breakdown of Definition df-nfOLD

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		vx	. . 3 setvar x
3	1, 2	wnfOLD 1709	. 2 wff F/ x ph
4	1, 2	wal 1481	. . . 4 wff A. x ph
5	1, 4	wi 4	. . 3 wff ( ph -> A. x ph )
6	5, 2	wal 1481	. 2 wff A. x ( ph -> A. x ph )
7	3, 6	wb 196	1 wff ( F/ x ph <-> A. x ( ph -> A. x ph ) )

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