Theorem nfs1v 1967

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

Syntax hints:  Ⅎwnf 1483  [wsb 1785

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786

This theorem is referenced by:  nfsbxy  1970  nfsbxyt  1971  sbco3v  1997  sbcomxyyz  2000  sbnf2  2009  mo2n  2082  mo23  2095  mor  2096  clelab  2331  cbvralf  2730  cbvrexf  2731  cbvralsv  2754  cbvrexsv  2755  cbvrab  2770  sbhypf  2822  mob2  2953  reu2  2961  sbcralt  3075  sbcrext  3076  sbcralg  3077  sbcreug  3079  sbcel12g  3108  sbceqg  3109  cbvreucsf  3158  cbvrabcsf  3159  disjiun  4039  cbvopab1  4117  cbvopab1s  4119  csbopabg  4122  cbvmptf  4138  cbvmpt  4139  opelopabsb  4306  frind  4399  tfis  4631  findes  4651  opeliunxp  4730  ralxpf  4824  rexxpf  4825  cbviota  5237  csbiotag  5264  isarep1  5360  cbvriota  5910  csbriotag  5912  abrexex2g  6205  abrexex2  6209  dfoprab4f  6279  finexdc  6999  ssfirab  7033  uzind4s  9711  zsupcllemstep  10372  bezoutlemmain  12319  nnwosdc  12360  cbvrald  15724  bj-bdfindes  15885  bj-findes  15917