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

Step	Hyp	Ref	Expression
1		hbs1 2105	. 2 ⊢ ([y / x]φ → ∀x[y / x]φ)
2	1	nfi 1551	1 ⊢ Ⅎx[y / x]φ

Syntax hints:  Ⅎ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:  sbnf2  2108  eu1  2225  mopick  2266  2mo  2282  2eu6  2289  clelab  2474  cbvralf  2830  cbvralsv  2847  cbvrexsv  2848  cbvrab  2858  sbhypf  2905  mob2  3017  reu2  3025  sbcralt  3119  sbcralg  3121  sbcrexg  3122  sbcreug  3123  sbcel12g  3152  sbceqg  3153  cbvreucsf  3201  cbvrabcsf  3202  csbifg  3691  cbviota  4345  csbiotag  4372  cbvopab1  4633  cbvopab1s  4635  csbopabg  4638  opelopabsb  4698  opeliunxp  4821  cbvmpt  5677