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  2696  cbvrexf  2697  cbvralsv  2719  cbvrexsv  2720  cbvrab  2735  sbhypf  2786  mob2  2917  reu2  2925  sbcralt  3039  sbcrext  3040  sbcralg  3041  sbcreug  3043  sbcel12g  3072  sbceqg  3073  cbvreucsf  3121  cbvrabcsf  3122  disjiun  3996  cbvopab1  4074  cbvopab1s  4076  csbopabg  4079  cbvmptf  4095  cbvmpt  4096  opelopabsb  4258  frind  4350  tfis  4580  findes  4600  opeliunxp  4679  ralxpf  4770  rexxpf  4771  cbviota  5180  csbiotag  5206  isarep1  5299  cbvriota  5836  csbriotag  5838  abrexex2g  6116  abrexex2  6120  dfoprab4f  6189  finexdc  6897  ssfirab  6928  uzind4s  9584  zsupcllemstep  11936  bezoutlemmain  11989  nnwosdc  12030  cbvrald  14311  bj-bdfindes  14472  bj-findes  14504