Theorem nfs1v 1951

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

Syntax hints:  Ⅎwnf 1471  [wsb 1773

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774

This theorem is referenced by:  nfsbxy  1954  nfsbxyt  1955  sbco3v  1981  sbcomxyyz  1984  sbnf2  1993  mo2n  2066  mo23  2079  mor  2080  clelab  2315  cbvralf  2714  cbvrexf  2715  cbvralsv  2738  cbvrexsv  2739  cbvrab  2754  sbhypf  2805  mob2  2936  reu2  2944  sbcralt  3058  sbcrext  3059  sbcralg  3060  sbcreug  3062  sbcel12g  3091  sbceqg  3092  cbvreucsf  3141  cbvrabcsf  3142  disjiun  4020  cbvopab1  4098  cbvopab1s  4100  csbopabg  4103  cbvmptf  4119  cbvmpt  4120  opelopabsb  4285  frind  4377  tfis  4607  findes  4627  opeliunxp  4706  ralxpf  4798  rexxpf  4799  cbviota  5208  csbiotag  5235  isarep1  5328  cbvriota  5872  csbriotag  5874  abrexex2g  6160  abrexex2  6164  dfoprab4f  6233  finexdc  6945  ssfirab  6977  uzind4s  9641  zsupcllemstep  12056  bezoutlemmain  12109  nnwosdc  12150  cbvrald  15204  bj-bdfindes  15365  bj-findes  15397