NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  nfsb GIF version

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
StepHypRef Expression
1 a16nf 2051 . 2 (z z = y → Ⅎz[y / x]φ)
2 nfsb.1 . . 3 zφ
32nfsb4 2081 . 2 z z = y → Ⅎz[y / x]φ)
41, 3pm2.61i 156 1 z[y / x]φ
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator