Theorem nfv 1581

Description: If x is not present in ph, then x is not free in ph. (Contributed by Mario Carneiro, 11-Aug-2016.)

Assertion

Ref	Expression
nfv	|- F/ x ph

Distinct variable group:   ph, x

Proof of Theorem nfv

Step	Hyp	Ref	Expression
1		ax-17 1579	. 2 |- ( ph -> A. x ph )
2	1	nfi 1515	1 |- F/ x ph

Syntax hints:   F/wnf 1513

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-gen 1502  ax-17 1579

This theorem depends on definitions:  df-bi 117  df-nf 1514

This theorem is referenced by:  nfvd  1582  alexim  1698  19.37aiv  1727  sbiedv  1842  spimv  1864  spimev  1914  19.36aiv  1957  cbval2  1977  cbvex2  1978  cbval2v  1979  cbvex2v  1980  cbvald  1981  cbvaldva  1984  cbvexdva  1985  eeanv  1992  nfsbv  2007  sbco2h  2024  nfsbt  2036  sbnf2  2041  dfsb7a  2054  sbalyz  2059  sbco4lem  2066  sbco4  2067  dvelimALT  2070  eubidv  2094  sb8eu  2099  nfeudv  2101  nfeud  2102  nfeuv  2104  nfeu  2105  mobidv  2122  mo23  2128  sbmo  2146  mo4  2148  moimv  2153  moanimv  2162  bm1.1  2223  eqsb1lem  2341  eqsb1  2342  clelsb1  2343  clelsb2  2344  abbibcom  2352  abbib  2356  abbidv  2358  cbvabv  2365  clelab  2366  nfcjust  2380  nfcv  2392  clelsb1f  2396  nfeqd  2407  nfeld  2408  nfabdw  2411  nfabd  2412  dvelimdc  2413  cleqf  2417  sbabel  2419  ralbidva  2546  rexbidva  2547  ralbidv  2550  rexbidv  2551  2ralbida  2571  2ralbidva  2572  nfraldya  2585  nfrexdya  2586  rgen2a  2604  ralimdva  2617  ralrimiv  2622  r19.21v  2627  ralrimdv  2629  reximdvai  2650  r19.23v  2660  rexlimiv  2662  rexlimdv  2667  r19.29af  2692  r19.29an  2693  r19.29a  2694  r19.32vr  2699  r19.37av  2704  r19.41v  2707  reean  2720  reeanv  2721  cbvrmow  2735  reubidva  2736  rmobidva  2741  cbvralf  2777  cbvrexf  2778  cbvreu  2784  cbvralv  2786  cbvrexv  2787  cbvreuv  2788  cbvrmov  2789  cbvralsv  2802  cbvrexsv  2803  sbralie  2804  cbvrab  2819  cbvrabv  2820  issetf  2829  ceqsalv  2852  ceqsralv  2853  ceqsexv  2861  ceqsex2  2863  ceqsex2v  2864  vtocld  2875  vtocl  2877  vtocl2  2878  vtocl3  2879  vtoclg  2883  vtocl2g  2887  vtoclga  2889  vtocl2gaf  2890  vtocl2ga  2891  vtocl3gaf  2892  vtocl3ga  2893  spcimdv  2909  spcimedv  2911  spcgv  2912  spcegv  2913  rspct  2922  rspc  2923  rspce  2924  rspcv  2925  rspcev  2929  rspc2v  2943  eqvincg  2950  eqvincf  2951  ceqsexgv  2955  elabgt  2967  elab  2970  elabg  2972  elab3g  2977  elrab3t  2981  elrab  2982  ralab2  2990  rexab2  2992  eqeu  2996  mosubt  3003  mo2icl  3005  mob2  3006  mob  3008  reu2  3014  reu3  3016  rmo4f  3024  nfcdeq  3048  sbcco  3073  sbcco2  3074  cbvsbcv  3081  sbcieg  3084  sbcie2g  3085  sbcied  3088  elrabsf  3090  sbcbidv  3110  sbcg  3121  sbc2iegf  3122  sbc2ie  3123  reu8nf  3133  rmo2ilem  3142  rmo3  3144  csbcow  3158  csbeq2dv  3173  nfcsb1d  3178  nfcsbd  3183  csbiebt  3187  csbied  3194  csbie2t  3196  sbcnestg  3201  sbnfc2  3208  cbvralcsf  3210  cbvrexcsf  3211  cbvreucsf  3212  cbvrabcsf  3213  cbvralv2  3214  cbvrexv2  3215  rspc2vd  3216  dfssf  3238  dfss2f  3239  uniiunlem  3338  abn0m  3547  rabn0m  3549  rabeq0  3552  abeq0  3553  r19.3rmv  3615  r19.28mv  3617  r19.27mv  3621  raaanv  3631  sbss  3632  nfifd  3665  rabsnifsb  3773  euabsn  3777  oprcl  3923  nfuni  3936  nfunid  3937  eluniab  3942  nfint  3975  elintab  3976  iineq2dv  4029  disjiun  4120  opabbidv  4192  nfopab  4194  cbvopab  4197  cbvopabv  4198  cbvopab1  4199  cbvopab2  4200  cbvopab1s  4201  cbvopab1v  4202  mpteq12f  4206  mpteq2dva  4216  cbvmptf  4220  cbvmpt  4221  zfrep6  4243  zfnuleu  4252  intexabim  4283  iinexgm  4285  repizf2  4294  bnd  4304  copsex2t  4380  copsex2g  4381  opelopabsb  4397  opelopabaf  4411  pofun  4452  frind  4492  reusv3  4601  alxfr  4602  rexxfrd  4604  ralxfrALT  4608  onintonm  4659  sucprcreg  4691  eunex  4703  tfis  4725  tfis2  4727  tfisi  4729  peano2  4737  findes  4745  omsinds  4764  opeliunxp  4825  opeliunxp2  4915  ralxpf  4921  rexxpf  4922  dfdmf  4969  reldmm  4995  dfrnf  5018  elrnmpt1  5028  intirr  5169  nfiotadw  5335  cbviota  5337  cbviotav  5339  sb8iota  5340  iota2d  5359  iota2  5362  dffun5r  5384  dffun6f  5385  dffun4f  5388  funco  5412  fun11  5443  imadif  5456  isarep1  5462  isarep2  5463  fun11iun  5655  fv3  5713  tz6.12f  5719  tz6.12c  5720  relelfvdm  5722  nfvres  5726  funimass4  5747  funfvdm2f  5762  fvmptss2  5774  fvmptdf  5787  fvmptdv  5788  fvmptt  5791  eqfnfv2f  5801  ralrnmpt  5841  rexrnmpt  5842  f1ompt  5850  ffnfv  5857  ffnfvf  5858  fmptco  5865  dfimafnf  5945  elabrex  5953  elabrexg  5954  dff13f  5966  fliftfun  5992  cbvriota  6040  cbvriotav  6041  riota2  6052  riotaeqimp  6053  riota5f  6055  acexmid  6074  nfoprab  6130  oprabbidv  6132  mpoeq123  6137  cbvoprab1  6150  cbvoprab2  6151  cbvoprab12  6152  cbvoprab12v  6153  cbvoprab3  6154  cbvoprab3v  6155  cbvmpox  6156  ralrnmpo  6193  ovmpodx  6205  ovmpodf  6210  ovmpodv  6211  ovi3  6216  ofrfval2  6309  abrexex2g  6339  opabex3d  6340  opabex3  6341  abrexex2  6343  elabreximdv  6347  uchoice  6361  dfoprab4f  6417  fmpox  6426  spc2ed  6459  cnvoprab  6460  f1od2  6461  opeliunxp2f  6499  tposoprab  6541  nfrecs  6568  tfri3  6628  nffrec  6657  eqerlem  6828  erovlem  6891  mptelixpg  7006  dom2lem  7048  modom  7098  xpf1o  7134  mapxpen  7138  nneneq  7148  findcard2  7183  findcard2s  7184  ac6sfi  7192  fiintim  7228  opabfi  7237  exmidomni  7472  fodjuomnilemdc  7474  ismkvnex  7485  mkvprop  7488  exmidfodomrlemr  7544  exmidfodomrlemrALT  7545  cc3  7624  indpi  7699  prarloclem3step  7853  prmuloc2  7924  ltexprlemm  7957  caucvgprprlemaddq  8065  caucvgsrlemgt1  8152  suplocsrlem  8165  axpre-suploclemres  8258  nn0ind-raph  9742  uzind4s  9969  indstr  9972  supinfneg  9974  infsupneg  9975  lbzbi  9995  fzrevral  10490  zsupcllemstep  10640  frecuzrdgtcl  10827  frecuzrdgfunlem  10834  nninfinf  10858  uzsinds  10859  seq3f1olemstep  10929  seq3f1olemp  10930  wrd2ind  11473  reuccatpfxs1  11497  fimaxre2  11971  climeu  12040  nfsum1  12100  nfsum  12101  sumrbdclem  12122  summodclem2a  12126  zsumdc  12129  fsum3  12132  isumss  12136  isumss2  12138  fsum3cvg2  12139  fsumsplitf  12153  fsum2dlemstep  12179  fsum00  12207  fsumrelem  12216  mertenslem2  12281  nfcprod1  12299  nfcprod  12300  prodeq2  12302  prodrbdclem  12316  prodmodclem2a  12321  zproddc  12324  fprodseq  12328  fprodntrivap  12329  prodssdc  12334  fprodcl2lem  12350  fprod2dlemstep  12367  fprodsplitf  12377  fprodsplit1f  12379  fprodap0f  12381  fprodle  12385  divalglemeunn  12666  divalglemeuneg  12668  bezoutlemnewy  12751  bezoutlemmain  12753  bezoutlemzz  12757  bezout  12766  nnwofdc  12793  prmind2  12876  oddpwdclemdvds  12926  oddpwdclemndvds  12927  pcmpt  13100  pcmptdvds  13102  exmidunben  13295  ctiunctlemfo  13308  ctiunct  13309  ctiunctal  13310  dfgrp3mlem  13880  gzsumsplit0  14125  gsumsncmn  14133  lss1d  14692  gsumfsum  14895  cnmpt11  15307  cnmpt21  15315  cnmptcom  15322  imasnopn  15323  mulcncf  15632  ellimc3apf  15684  limccnp2cntop  15701  dvmptfsum  15749  lgseisenlem2  16104  gropd  16202  grstructd2dom  16203  ch2varv  16710  elab1  16725  elab2a  16726  elabg2  16727  cbvrald  16730  sumdc2  16741  bdsepnft  16827  bdsepnfALT  16829  bj-omssind  16875  bj-bdfindes  16889  bj-nn0suc0  16890  bj-nntrans  16891  bj-nnelirr  16893  bj-omtrans  16896  setindft  16905  bj-inf2vnlem3  16912  bj-inf2vnlem4  16913  bj-nn0sucALT  16918  bj-findis  16919  bj-findes  16921  strcollnft  16924  strcollnfALT  16926  pw1nct  16947  isomninnlem  16984  trilpolemeq1  16994  trirec0  16998  iswomninnlem  17004  ismkvnnlem  17007  nconstwlpolemgt0  17019