Theorem nfs1v 1968

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 1967	. 2 ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
2	1	nfi 1486	1 ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑

Syntax hints:  Ⅎwnf 1484  [wsb 1786

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787

This theorem is referenced by:  nfsbxy  1971  nfsbxyt  1972  sbco3v  1998  sbcomxyyz  2001  sbnf2  2010  mo2n  2083  mo23  2097  mor  2098  clelab  2333  cbvralf  2733  cbvrexf  2734  cbvralsv  2758  cbvrexsv  2759  cbvrab  2774  sbhypf  2827  mob2  2960  reu2  2968  sbcralt  3082  sbcrext  3083  sbcralg  3084  sbcreug  3086  sbcel12g  3116  sbceqg  3117  cbvreucsf  3166  cbvrabcsf  3167  disjiun  4054  cbvopab1  4133  cbvopab1s  4135  csbopabg  4138  cbvmptf  4154  cbvmpt  4155  opelopabsb  4324  frind  4417  tfis  4649  findes  4669  opeliunxp  4748  ralxpf  4842  rexxpf  4843  cbviota  5256  csbiotag  5283  isarep1  5379  cbvriota  5933  csbriotag  5935  abrexex2g  6228  abrexex2  6232  dfoprab4f  6302  finexdc  7025  ssfirab  7059  uzind4s  9746  zsupcllemstep  10409  bezoutlemmain  12434  nnwosdc  12475  cbvrald  15924  bj-bdfindes  16084  bj-findes  16116