Definition df-nf 1449

Description: Define the not-free predicate for wffs. This is read " x is not free in ph". Not-free means that the value of x cannot affect the value of ph, e.g., any occurrence of x in ph is effectively bound by a "for all" or something that expands to one (such as "there exists"). In particular, substitution for a variable not free in a wff does not affect its value (sbf 1765). An example of where this is used is stdpc5 1572. See nf2 1656 for an alternate definition which does not involve nested quantifiers on the same variable.

Nonfreeness is a commonly used condition, so it is useful to have a notation for it. Surprisingly, there is no common formal notation for it, so here we devise one. Our definition lets us work with the notion of nonfreeness within the logic itself rather than as a metalogical side condition.

To be precise, our definition really means "effectively not free", because it is slightly less restrictive than the usual textbook definition for "not free" (which considers syntactic freedom). For example, x is effectively not free in the expression x = x (even though x is syntactically free in it, so would be considered "free" in the usual textbook definition) because the value of x in the formula x = x does not affect the truth of that formula (and thus substitutions will not change the result), see nfequid 1690. (Contributed by Mario Carneiro, 11-Aug-2016.)

Assertion

Ref	Expression
df-nf	|- ( F/ x ph <-> A. x ( ph -> A. x ph ) )

Detailed syntax breakdown of Definition df-nf

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		vx	. . 3 setvar x
3	1, 2	wnf 1448	. 2 wff F/ x ph
4	1, 2	wal 1341	. . . 4 wff A. x ph
5	1, 4	wi 4	. . 3 wff ( ph -> A. x ph )
6	5, 2	wal 1341	. 2 wff A. x ( ph -> A. x ph )
7	3, 6	wb 104	1 wff ( F/ x ph <-> A. x ( ph -> A. x ph ) )

This definition is referenced by:  nfi  1450  nfbii  1461  nfr  1506  nfd  1511  nfbidf  1527  nfnf1  1532  nford  1555  nfand  1556  nfal  1564  nfnf  1565  nfalt  1566  19.21t  1570  nfimd  1573  19.9t  1630  nfnt  1644  nf2  1656  drnf1  1721  drnf2  1722  nfexd  1749  dveeq2or  1804  nfsb2or  1825  nfdv  1865  nfsbxy  1930  nfsbxyt  1931  sbcomxyyz  1960  sbnf2  1969  dvelimALT  1998  dvelimfv  1999  nfsb4t  2002  dvelimor  2006  oprabidlem  5869  bj-nfalt  13605