Theorem nfv 1538

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

Syntax hints:   F/wnf 1470

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 1459  ax-17 1536

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

This theorem is referenced by:  nfvd  1539  alexim  1655  19.37aiv  1685  sbiedv  1799  spimv  1821  spimev  1871  19.36aiv  1911  cbval2  1931  cbvex2  1932  cbval2v  1933  cbvex2v  1934  cbvald  1935  cbvaldva  1938  cbvexdva  1939  eeanv  1942  nfsbv  1957  sbco2h  1974  nfsbt  1986  sbnf2  1991  dfsb7a  2004  sbalyz  2009  sbco4lem  2016  sbco4  2017  dvelimALT  2020  eubidv  2044  sb8eu  2049  nfeudv  2051  nfeud  2052  nfeuv  2054  nfeu  2055  mobidv  2072  mo23  2077  sbmo  2095  mo4  2097  moimv  2102  moanimv  2111  bm1.1  2172  eqsb1lem  2290  eqsb1  2291  clelsb1  2292  clelsb2  2293  abbi  2301  abbidv  2305  cbvabv  2312  clelab  2313  nfcjust  2317  nfcv  2329  clelsb1f  2333  nfeqd  2344  nfeld  2345  nfabdw  2348  nfabd  2349  dvelimdc  2350  cleqf  2354  sbabel  2356  ralbidva  2483  rexbidva  2484  ralbidv  2487  rexbidv  2488  2ralbida  2508  2ralbidva  2509  nfraldya  2522  nfrexdya  2523  rgen2a  2541  ralimdva  2554  ralrimiv  2559  r19.21v  2564  ralrimdv  2566  reximdvai  2587  r19.23v  2596  rexlimiv  2598  rexlimdv  2603  r19.29af  2628  r19.29an  2629  r19.29a  2630  r19.32vr  2635  r19.37av  2640  r19.41v  2643  reean  2656  reeanv  2657  reubidva  2670  rmobidva  2675  cbvralf  2707  cbvrexf  2708  cbvreu  2713  cbvralv  2715  cbvrexv  2716  cbvreuv  2717  cbvrmov  2718  cbvralsv  2731  cbvrexsv  2732  sbralie  2733  cbvrab  2747  cbvrabv  2748  issetf  2756  ceqsalv  2779  ceqsralv  2780  ceqsexv  2788  ceqsex2  2789  ceqsex2v  2790  vtocld  2801  vtocl  2803  vtocl2  2804  vtocl3  2805  vtoclg  2809  vtocl2g  2813  vtoclga  2815  vtocl2gaf  2816  vtocl2ga  2817  vtocl3gaf  2818  vtocl3ga  2819  spcimdv  2833  spcimedv  2835  spcgv  2836  spcegv  2837  rspct  2846  rspc  2847  rspce  2848  rspcv  2849  rspcev  2853  rspc2v  2866  eqvincg  2873  eqvincf  2874  ceqsexgv  2878  elabgt  2890  elab  2893  elabg  2895  elab3g  2900  elrab3t  2904  elrab  2905  ralab2  2913  rexab2  2915  eqeu  2919  mosubt  2926  mo2icl  2928  mob2  2929  mob  2931  reu2  2937  reu3  2939  rmo4f  2947  nfcdeq  2971  sbcco  2996  sbcco2  2997  cbvsbcv  3004  sbcieg  3007  sbcie2g  3008  sbcied  3011  elrabsf  3013  sbcbidv  3033  sbcg  3044  sbc2iegf  3045  sbc2ie  3046  rmo2ilem  3064  rmo3  3066  csbcow  3080  csbeq2dv  3095  nfcsb1d  3100  nfcsbd  3104  csbiebt  3108  csbied  3115  csbie2t  3117  sbcnestg  3122  sbnfc2  3129  cbvralcsf  3131  cbvrexcsf  3132  cbvreucsf  3133  cbvrabcsf  3134  cbvralv2  3135  cbvrexv2  3136  rspc2vd  3137  dfss2f  3158  uniiunlem  3256  abn0m  3460  rabn0m  3462  rabeq0  3464  abeq0  3465  r19.3rmv  3525  r19.28mv  3527  r19.27mv  3531  raaanv  3542  sbss  3543  nfifd  3573  euabsn  3674  oprcl  3814  nfuni  3827  nfunid  3828  eluniab  3833  nfint  3866  elintab  3867  iineq2dv  3920  disjiun  4010  opabbidv  4081  nfopab  4083  cbvopab  4086  cbvopabv  4087  cbvopab1  4088  cbvopab2  4089  cbvopab1s  4090  cbvopab1v  4091  mpteq12f  4095  mpteq2dva  4105  cbvmptf  4109  cbvmpt  4110  zfrep6  4132  zfnuleu  4139  intexabim  4164  iinexgm  4166  repizf2  4174  bnd  4184  copsex2t  4257  copsex2g  4258  opelopabsb  4272  opelopabaf  4285  pofun  4324  frind  4364  reusv3  4472  alxfr  4473  rexxfrd  4475  ralxfrALT  4479  onintonm  4528  sucprcreg  4560  eunex  4572  tfis  4594  tfis2  4596  tfisi  4598  peano2  4606  findes  4614  omsinds  4633  opeliunxp  4693  opeliunxp2  4779  ralxpf  4785  rexxpf  4786  dfdmf  4832  dfrnf  4880  elrnmpt1  4890  intirr  5027  nfiotadw  5193  cbviota  5195  cbviotav  5196  sb8iota  5197  iota2d  5215  iota2  5218  dffun5r  5240  dffun6f  5241  dffun4f  5244  funco  5268  fun11  5295  imadif  5308  isarep1  5314  isarep2  5315  fun11iun  5494  fv3  5550  tz6.12f  5556  tz6.12c  5557  relelfvdm  5559  nfvres  5560  funimass4  5579  funfvdm2f  5594  fvmptss2  5604  fvmptdf  5616  fvmptdv  5617  fvmptt  5620  eqfnfv2f  5630  ralrnmpt  5671  rexrnmpt  5672  f1ompt  5680  ffnfv  5687  ffnfvf  5688  fmptco  5695  elabrex  5771  elabrexg  5772  dff13f  5784  fliftfun  5810  cbvriota  5854  cbvriotav  5855  riota2  5866  riota5f  5868  acexmid  5887  nfoprab  5940  oprabbidv  5942  mpoeq123  5947  cbvoprab1  5960  cbvoprab2  5961  cbvoprab12  5962  cbvoprab12v  5963  cbvoprab3  5964  cbvoprab3v  5965  cbvmpox  5966  ralrnmpo  6003  ovmpodx  6015  ovmpodf  6020  ovmpodv  6021  ovi3  6025  ofrfval2  6113  abrexex2g  6135  opabex3d  6136  opabex3  6137  abrexex2  6139  dfoprab4f  6208  fmpox  6215  spc2ed  6248  cnvoprab  6249  f1od2  6250  opeliunxp2f  6253  tposoprab  6295  nfrecs  6322  tfri3  6382  nffrec  6411  eqerlem  6580  erovlem  6641  mptelixpg  6748  dom2lem  6786  xpf1o  6858  mapxpen  6862  nneneq  6871  findcard2  6903  findcard2s  6904  ac6sfi  6912  fiintim  6942  exmidomni  7154  fodjuomnilemdc  7156  ismkvnex  7167  mkvprop  7170  exmidfodomrlemr  7215  exmidfodomrlemrALT  7216  cc3  7281  indpi  7355  prarloclem3step  7509  prmuloc2  7580  ltexprlemm  7613  caucvgprprlemaddq  7721  caucvgsrlemgt1  7808  suplocsrlem  7821  axpre-suploclemres  7914  nn0ind-raph  9384  uzind4s  9604  indstr  9607  supinfneg  9609  infsupneg  9610  lbzbi  9630  fzrevral  10119  frecuzrdgtcl  10426  frecuzrdgfunlem  10433  uzsinds  10456  seq3f1olemstep  10515  seq3f1olemp  10516  fimaxre2  11249  climeu  11318  nfsum1  11378  nfsum  11379  sumrbdclem  11399  summodclem2a  11403  zsumdc  11406  fsum3  11409  isumss  11413  isumss2  11415  fsum3cvg2  11416  fsumsplitf  11430  fsum2dlemstep  11456  fsum00  11484  fsumrelem  11493  mertenslem2  11558  nfcprod1  11576  nfcprod  11577  prodeq2  11579  prodrbdclem  11593  prodmodclem2a  11598  zproddc  11601  fprodseq  11605  fprodntrivap  11606  prodssdc  11611  fprodcl2lem  11627  fprod2dlemstep  11644  fprodsplitf  11654  fprodsplit1f  11656  fprodap0f  11658  fprodle  11662  divalglemeunn  11940  divalglemeuneg  11942  zsupcllemstep  11960  bezoutlemnewy  12011  bezoutlemmain  12013  bezoutlemzz  12017  bezout  12026  nnwofdc  12053  prmind2  12134  oddpwdclemdvds  12184  oddpwdclemndvds  12185  pcmpt  12355  pcmptdvds  12357  exmidunben  12441  ctiunctlemfo  12454  ctiunct  12455  ctiunctal  12456  dfgrp3mlem  12995  lss1d  13572  cnmpt11  14079  cnmpt21  14087  cnmptcom  14094  imasnopn  14095  mulcncf  14387  ellimc3apf  14425  limccnp2cntop  14442  lgseisenlem2  14747  ch2varv  14816  elab1  14831  elab2a  14832  elabg2  14833  cbvrald  14836  sumdc2  14847  bdsepnft  14935  bdsepnfALT  14937  bj-omssind  14983  bj-bdfindes  14997  bj-nn0suc0  14998  bj-nntrans  14999  bj-nnelirr  15001  bj-omtrans  15004  setindft  15013  bj-inf2vnlem3  15020  bj-inf2vnlem4  15021  bj-nn0sucALT  15026  bj-findis  15027  bj-findes  15029  strcollnft  15032  strcollnfALT  15034  pw1nct  15049  isomninnlem  15075  trilpolemeq1  15085  trirec0  15089  iswomninnlem  15094  ismkvnnlem  15097  nconstwlpolemgt0  15109