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  2710  cbvrexf  2711  cbvralsv  2734  cbvrexsv  2735  cbvrab  2750  sbhypf  2801  mob2  2932  reu2  2940  sbcralt  3054  sbcrext  3055  sbcralg  3056  sbcreug  3058  sbcel12g  3087  sbceqg  3088  cbvreucsf  3136  cbvrabcsf  3137  disjiun  4013  cbvopab1  4091  cbvopab1s  4093  csbopabg  4096  cbvmptf  4112  cbvmpt  4113  opelopabsb  4275  frind  4367  tfis  4597  findes  4617  opeliunxp  4696  ralxpf  4788  rexxpf  4789  cbviota  5198  csbiotag  5225  isarep1  5318  cbvriota  5858  csbriotag  5860  abrexex2g  6140  abrexex2  6144  dfoprab4f  6213  finexdc  6921  ssfirab  6952  uzind4s  9610  zsupcllemstep  11966  bezoutlemmain  12019  nnwosdc  12060  cbvrald  14944  bj-bdfindes  15105  bj-findes  15137