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  2471  cbvralf  2829  cbvreu  2833  cbvralsv  2846  cbvrexsv  2847  cbvrab  2857  cbvreucsf  3200  cbvrabcsf  3201  cbviota  4344  sb8iota  4346  cbvopab1  4632  ralxpf  4827  cbvmpt  5676