Theorem nfv 1516

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 1514	. 2 |- ( ph -> A. x ph )
2	1	nfi 1450	1 |- F/ x ph

Syntax hints:   F/wnf 1448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1437  ax-17 1514

This theorem depends on definitions:  df-bi 116  df-nf 1449

This theorem is referenced by:  nfvd  1517  alexim  1633  19.37aiv  1663  sbiedv  1777  spimv  1799  spimev  1849  19.36aiv  1889  cbval2  1909  cbvex2  1910  cbval2v  1911  cbvex2v  1912  cbvald  1913  cbvaldva  1916  cbvexdva  1917  eeanv  1920  nfsbv  1935  sbco2h  1952  nfsbt  1964  sbnf2  1969  dfsb7a  1982  sbalyz  1987  sbco4lem  1994  sbco4  1995  dvelimALT  1998  eubidv  2022  sb8eu  2027  nfeudv  2029  nfeud  2030  nfeuv  2032  nfeu  2033  mobidv  2050  mo23  2055  sbmo  2073  mo4  2075  moimv  2080  moanimv  2089  bm1.1  2150  eqsb1lem  2269  eqsb1  2270  clelsb1  2271  clelsb2  2272  abbi  2280  abbidv  2284  cbvabv  2291  clelab  2292  nfcjust  2296  nfcv  2308  clelsb1f  2312  nfeqd  2323  nfeld  2324  nfabdw  2327  nfabd  2328  dvelimdc  2329  cleqf  2333  sbabel  2335  ralbidva  2462  rexbidva  2463  ralbidv  2466  rexbidv  2467  2ralbida  2487  2ralbidva  2488  nfraldya  2501  nfrexdya  2502  rgen2a  2520  ralimdva  2533  ralrimiv  2538  r19.21v  2543  ralrimdv  2545  reximdvai  2566  r19.23v  2575  rexlimiv  2577  rexlimdv  2582  r19.29af  2607  r19.29an  2608  r19.29a  2609  r19.32vr  2614  r19.37av  2619  r19.41v  2622  reean  2634  reeanv  2635  reubidva  2648  rmobidva  2653  cbvralf  2685  cbvrexf  2686  cbvreu  2690  cbvralv  2692  cbvrexv  2693  cbvreuv  2694  cbvrmov  2695  cbvralsv  2708  cbvrexsv  2709  sbralie  2710  cbvrab  2724  cbvrabv  2725  issetf  2733  ceqsalv  2756  ceqsralv  2757  ceqsexv  2765  ceqsex2  2766  ceqsex2v  2767  vtocld  2778  vtocl  2780  vtocl2  2781  vtocl3  2782  vtoclg  2786  vtocl2g  2790  vtoclga  2792  vtocl2gaf  2793  vtocl2ga  2794  vtocl3gaf  2795  vtocl3ga  2796  spcimdv  2810  spcimedv  2812  spcgv  2813  spcegv  2814  rspct  2823  rspc  2824  rspce  2825  rspcv  2826  rspcev  2830  rspc2v  2843  eqvincg  2850  eqvincf  2851  ceqsexgv  2855  elabgt  2867  elab  2870  elabg  2872  elab3g  2877  elrab3t  2881  elrab  2882  ralab2  2890  rexab2  2892  eqeu  2896  mosubt  2903  mo2icl  2905  mob2  2906  mob  2908  reu2  2914  reu3  2916  rmo4f  2924  nfcdeq  2948  sbcco  2972  sbcco2  2973  cbvsbcv  2980  sbcieg  2983  sbcie2g  2984  sbcied  2987  elrabsf  2989  sbcbidv  3009  sbcg  3020  sbc2iegf  3021  sbc2ie  3022  rmo2ilem  3040  rmo3  3042  csbcow  3056  csbeq2dv  3071  nfcsb1d  3076  nfcsbd  3080  csbiebt  3084  csbied  3091  csbie2t  3093  sbcnestg  3098  sbnfc2  3105  cbvralcsf  3107  cbvrexcsf  3108  cbvreucsf  3109  cbvrabcsf  3110  cbvralv2  3111  cbvrexv2  3112  dfss2f  3133  uniiunlem  3231  abn0m  3434  rabn0m  3436  rabeq0  3438  abeq0  3439  r19.3rmv  3499  r19.28mv  3501  r19.27mv  3505  raaanv  3516  sbss  3517  nfifd  3547  euabsn  3646  oprcl  3782  nfuni  3795  nfunid  3796  eluniab  3801  nfint  3834  elintab  3835  iineq2dv  3888  disjiun  3977  opabbidv  4048  nfopab  4050  cbvopab  4053  cbvopabv  4054  cbvopab1  4055  cbvopab2  4056  cbvopab1s  4057  cbvopab1v  4058  mpteq12f  4062  mpteq2dva  4072  cbvmptf  4076  cbvmpt  4077  zfrep6  4099  zfnuleu  4106  intexabim  4131  iinexgm  4133  repizf2  4141  bnd  4151  copsex2t  4223  copsex2g  4224  opelopabsb  4238  opelopabaf  4251  pofun  4290  frind  4330  reusv3  4438  alxfr  4439  rexxfrd  4441  ralxfrALT  4445  onintonm  4494  sucprcreg  4526  eunex  4538  tfis  4560  tfis2  4562  tfisi  4564  peano2  4572  findes  4580  omsinds  4599  opeliunxp  4659  opeliunxp2  4744  ralxpf  4750  rexxpf  4751  dfdmf  4797  dfrnf  4845  elrnmpt1  4855  intirr  4990  nfiotadw  5156  cbviota  5158  cbviotav  5159  sb8iota  5160  iota2d  5178  iota2  5179  dffun5r  5200  dffun6f  5201  dffun4f  5204  funco  5228  fun11  5255  imadif  5268  isarep1  5274  isarep2  5275  fun11iun  5453  fv3  5509  tz6.12f  5515  tz6.12c  5516  relelfvdm  5518  nfvres  5519  funimass4  5537  funfvdm2f  5551  fvmptss2  5561  fvmptdf  5573  fvmptdv  5574  fvmptt  5577  eqfnfv2f  5587  ralrnmpt  5627  rexrnmpt  5628  f1ompt  5636  ffnfv  5643  ffnfvf  5644  fmptco  5651  elabrex  5726  dff13f  5738  fliftfun  5764  cbvriota  5808  cbvriotav  5809  riota2  5820  riota5f  5822  acexmid  5841  nfoprab  5894  oprabbidv  5896  mpoeq123  5901  cbvoprab1  5914  cbvoprab2  5915  cbvoprab12  5916  cbvoprab12v  5917  cbvoprab3  5918  cbvoprab3v  5919  cbvmpox  5920  ralrnmpo  5956  ovmpodx  5968  ovmpodf  5973  ovmpodv  5974  ovi3  5978  ofrfval2  6066  abrexex2g  6088  opabex3d  6089  opabex3  6090  abrexex2  6092  dfoprab4f  6161  fmpox  6168  spc2ed  6201  cnvoprab  6202  f1od2  6203  opeliunxp2f  6206  tposoprab  6248  nfrecs  6275  tfri3  6335  nffrec  6364  eqerlem  6532  erovlem  6593  mptelixpg  6700  dom2lem  6738  xpf1o  6810  mapxpen  6814  nneneq  6823  findcard2  6855  findcard2s  6856  ac6sfi  6864  fiintim  6894  exmidomni  7106  fodjuomnilemdc  7108  ismkvnex  7119  mkvprop  7122  exmidfodomrlemr  7158  exmidfodomrlemrALT  7159  cc3  7209  indpi  7283  prarloclem3step  7437  prmuloc2  7508  ltexprlemm  7541  caucvgprprlemaddq  7649  caucvgsrlemgt1  7736  suplocsrlem  7749  axpre-suploclemres  7842  nn0ind-raph  9308  uzind4s  9528  indstr  9531  supinfneg  9533  infsupneg  9534  lbzbi  9554  fzrevral  10040  frecuzrdgtcl  10347  frecuzrdgfunlem  10354  uzsinds  10377  seq3f1olemstep  10436  seq3f1olemp  10437  fimaxre2  11168  climeu  11237  nfsum1  11297  nfsum  11298  sumrbdclem  11318  summodclem2a  11322  zsumdc  11325  fsum3  11328  isumss  11332  isumss2  11334  fsum3cvg2  11335  fsumsplitf  11349  fsum2dlemstep  11375  fsum00  11403  fsumrelem  11412  mertenslem2  11477  nfcprod1  11495  nfcprod  11496  prodeq2  11498  prodrbdclem  11512  prodmodclem2a  11517  zproddc  11520  fprodseq  11524  fprodntrivap  11525  prodssdc  11530  fprodcl2lem  11546  fprod2dlemstep  11563  fprodsplitf  11573  fprodsplit1f  11575  fprodap0f  11577  fprodle  11581  divalglemeunn  11858  divalglemeuneg  11860  zsupcllemstep  11878  bezoutlemnewy  11929  bezoutlemmain  11931  bezoutlemzz  11935  bezout  11944  nnwofdc  11971  prmind2  12052  oddpwdclemdvds  12102  oddpwdclemndvds  12103  pcmpt  12273  pcmptdvds  12275  exmidunben  12359  ctiunctlemfo  12372  ctiunct  12373  ctiunctal  12374  cnmpt11  12923  cnmpt21  12931  cnmptcom  12938  imasnopn  12939  mulcncf  13231  ellimc3apf  13269  limccnp2cntop  13286  ch2varv  13649  elab1  13664  elab2a  13665  elabg2  13666  cbvrald  13669  sumdc2  13680  bdsepnft  13769  bdsepnfALT  13771  bj-omssind  13817  bj-bdfindes  13831  bj-nn0suc0  13832  bj-nntrans  13833  bj-nnelirr  13835  bj-omtrans  13838  setindft  13847  bj-inf2vnlem3  13854  bj-inf2vnlem4  13855  bj-nn0sucALT  13860  bj-findis  13861  bj-findes  13863  strcollnft  13866  strcollnfALT  13868  pw1nct  13883  isomninnlem  13909  trilpolemeq1  13919  trirec0  13923  iswomninnlem  13928  ismkvnnlem  13931  nconstwlpolemgt0  13942