Theorem nfs1v 1939

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

Syntax hints:  Ⅎwnf 1460  [wsb 1762

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763

This theorem is referenced by:  nfsbxy  1942  nfsbxyt  1943  sbco3v  1969  sbcomxyyz  1972  sbnf2  1981  mo2n  2054  mo23  2067  mor  2068  clelab  2303  cbvralf  2697  cbvrexf  2698  cbvralsv  2720  cbvrexsv  2721  cbvrab  2736  sbhypf  2787  mob2  2918  reu2  2926  sbcralt  3040  sbcrext  3041  sbcralg  3042  sbcreug  3044  sbcel12g  3073  sbceqg  3074  cbvreucsf  3122  cbvrabcsf  3123  disjiun  3999  cbvopab1  4077  cbvopab1s  4079  csbopabg  4082  cbvmptf  4098  cbvmpt  4099  opelopabsb  4261  frind  4353  tfis  4583  findes  4603  opeliunxp  4682  ralxpf  4774  rexxpf  4775  cbviota  5184  csbiotag  5210  isarep1  5303  cbvriota  5841  csbriotag  5843  abrexex2g  6121  abrexex2  6125  dfoprab4f  6194  finexdc  6902  ssfirab  6933  uzind4s  9590  zsupcllemstep  11946  bezoutlemmain  11999  nnwosdc  12040  cbvrald  14543  bj-bdfindes  14704  bj-findes  14736