Theorem nfs1v 1992

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

Syntax hints:  Ⅎwnf 1509  [wsb 1810

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811

This theorem is referenced by:  nfsbxy  1995  nfsbxyt  1996  sbco3v  2022  sbcomxyyz  2025  sbnf2  2034  mo2n  2107  mo23  2121  mor  2122  clelab  2358  cbvralf  2759  cbvrexf  2760  cbvralsv  2784  cbvrexsv  2785  cbvrab  2801  sbhypf  2854  mob2  2987  reu2  2995  sbcralt  3109  sbcrext  3110  sbcralg  3111  sbcreug  3113  sbcel12g  3143  sbceqg  3144  cbvreucsf  3193  cbvrabcsf  3194  disjiun  4088  cbvopab1  4167  cbvopab1s  4169  csbopabg  4172  cbvmptf  4188  cbvmpt  4189  opelopabsb  4360  frind  4455  tfis  4687  findes  4707  opeliunxp  4787  ralxpf  4882  rexxpf  4883  cbviota  5298  csbiotag  5326  isarep1  5423  cbvriota  5993  csbriotag  5995  abrexex2g  6291  abrexex2  6295  dfoprab4f  6365  modom  7037  finexdc  7135  ssfirab  7172  uzind4s  9868  zsupcllemstep  10535  bezoutlemmain  12632  nnwosdc  12673  cbvrald  16489  bj-bdfindes  16648  bj-findes  16680