Theorem nfsb 2109

Description: If z is not free in φ, it is not free in [y / x]φ when y and z are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.)

Hypothesis

Ref	Expression
nfsb.1	⊢ Ⅎzφ

Assertion

Ref	Expression
nfsb	⊢ Ⅎz[y / x]φ

Distinct variable group:   y,z

Allowed substitution hints:   φ(x,y,z)

Proof of Theorem nfsb

Step	Hyp	Ref	Expression
1		a16nf 2051	. 2 ⊢ (∀z z = y → Ⅎz[y / x]φ)
2		nfsb.1	. . 3 ⊢ Ⅎzφ
3	2	nfsb4 2081	. 2 ⊢ (¬ ∀z z = y → Ⅎz[y / x]φ)
4	1, 3	pm2.61i 156	1 ⊢ Ⅎz[y / x]φ

Syntax hints:  ∀wal 1540  Ⅎwnf 1544  [wsb 1648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925

This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649

This theorem is referenced by:  hbsb  2110  2sb5rf  2117  2sb6rf  2118  sb10f  2122  sb8eu  2222  2mo  2282  2eu6  2289  cbvab  2472  cbvralf  2830  cbvreu  2834  cbvralsv  2847  cbvrexsv  2848  cbvrab  2858  cbvreucsf  3201  cbvrabcsf  3202  cbviota  4345  sb8iota  4347  cbvopab1  4633  ralxpf  4828  cbvmpt  5677