Theorem nfs1v 1999

Description: 𝑥 is not free in [𝑦 / 𝑥]𝜑 when 𝑥 and 𝑦 are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.)

Assertion

Ref	Expression
nfs1v	⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑

Distinct variable group:   𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem nfs1v

Step	Hyp	Ref	Expression
1		hbs1 1998	. 2 ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
2	1	nfi 1515	1 ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑

Syntax hints:  Ⅎwnf 1513  [wsb 1815

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816

This theorem is referenced by:  nfsbxy  2002  nfsbxyt  2003  sbco3v  2029  sbcomxyyz  2032  sbnf2  2041  mo2n  2114  mo23  2128  mor  2129  clelab  2366  cbvralf  2777  cbvrexf  2778  cbvralsv  2802  cbvrexsv  2803  cbvrab  2819  sbhypf  2872  mob2  3006  reu2  3014  sbcralt  3128  sbcrext  3129  sbcralg  3130  sbcreug  3132  sbcel12g  3162  sbceqg  3163  cbvreucsf  3212  cbvrabcsf  3213  disjiun  4120  cbvopab1  4199  cbvopab1s  4201  csbopabg  4204  cbvmptf  4220  cbvmpt  4221  opelopabsb  4397  frind  4492  tfis  4725  findes  4745  opeliunxp  4825  ralxpf  4921  rexxpf  4922  cbviota  5337  csbiotag  5365  isarep1  5462  cbvriota  6040  csbriotag  6042  abrexex2g  6339  abrexex2  6343  dfoprab4f  6417  modom  7098  finexdc  7197  ssfirab  7234  uzind4s  9969  zsupcllemstep  10640  bezoutlemmain  12753  nnwosdc  12794  cbvrald  16730  bj-bdfindes  16889  bj-findes  16921