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

Theorem nfs1v 2106
 Description: x is not free in [y / x]φ when x and y are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.)
Assertion
Ref Expression
nfs1v x[y / x]φ
Distinct variable group:   x,y
Allowed substitution hints:   φ(x,y)

Proof of Theorem nfs1v
StepHypRef Expression
1 hbs1 2105 . 2 ([y / x]φx[y / x]φ)
21nfi 1551 1 x[y / x]φ
 Colors of variables: wff setvar class Syntax hints:  Ⅎwnf 1544  [wsb 1648 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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:  sbnf2  2108  eu1  2225  mopick  2266  2mo  2282  2eu6  2289  clelab  2473  cbvralf  2829  cbvralsv  2846  cbvrexsv  2847  cbvrab  2857  sbhypf  2904  mob2  3016  reu2  3024  sbcralt  3118  sbcralg  3120  sbcrexg  3121  sbcreug  3122  sbcel12g  3151  sbceqg  3152  cbvreucsf  3200  cbvrabcsf  3201  csbifg  3690  cbviota  4344  csbiotag  4371  cbvopab1  4632  cbvopab1s  4634  csbopabg  4637  opelopabsb  4697  opeliunxp  4820  cbvmpt  5676
 Copyright terms: Public domain W3C validator