Theorem nfs1v 1939

Description: x is not free in [ y / x ] ph when x and y are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.)

Assertion

Ref	Expression
nfs1v	|- F/ x [ y / x ] ph

Distinct variable group:   x, y

Allowed substitution hints:   ph( x, y)

Proof of Theorem nfs1v

Step	Hyp	Ref	Expression
1		hbs1 1938	. 2 |- ( [ y / x ] ph -> A. x [ y / x ] ph )
2	1	nfi 1462	1 |- F/ x [ y / x ] ph

Syntax hints:   F/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  2721  cbvrexsv  2722  cbvrab  2737  sbhypf  2788  mob2  2919  reu2  2927  sbcralt  3041  sbcrext  3042  sbcralg  3043  sbcreug  3045  sbcel12g  3074  sbceqg  3075  cbvreucsf  3123  cbvrabcsf  3124  disjiun  4000  cbvopab1  4078  cbvopab1s  4080  csbopabg  4083  cbvmptf  4099  cbvmpt  4100  opelopabsb  4262  frind  4354  tfis  4584  findes  4604  opeliunxp  4683  ralxpf  4775  rexxpf  4776  cbviota  5185  csbiotag  5211  isarep1  5304  cbvriota  5843  csbriotag  5845  abrexex2g  6123  abrexex2  6127  dfoprab4f  6196  finexdc  6904  ssfirab  6935  uzind4s  9592  zsupcllemstep  11948  bezoutlemmain  12001  nnwosdc  12042  cbvrald  14625  bj-bdfindes  14786  bj-findes  14818