Theorem nfv 1508

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

Syntax hints:   F/wnf 1436

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 1425  ax-17 1506

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

This theorem is referenced by:  nfvd  1509  alexim  1624  19.37aiv  1653  sbiedv  1762  spimv  1783  spimev  1833  19.36aiv  1873  cbval2  1891  cbvex2  1892  cbval2v  1893  cbvex2v  1894  cbvald  1895  cbvaldva  1898  cbvexdva  1899  eeanv  1902  sbco2h  1935  nfsbt  1947  sbnf2  1954  dfsb7a  1967  sbalyz  1972  sbco4lem  1979  sbco4  1980  dvelimALT  1983  eubidv  2005  sb8eu  2010  nfeudv  2012  nfeud  2013  nfeuv  2015  nfeu  2016  mobidv  2033  mo23  2038  sbmo  2056  mo4  2058  moimv  2063  moanimv  2072  bm1.1  2122  eqsb3lem  2240  eqsb3  2241  clelsb3  2242  clelsb4  2243  abbi  2251  abbidv  2255  cbvabv  2262  clelab  2263  nfcjust  2267  nfcv  2279  clelsb3f  2283  nfeqd  2294  nfeld  2295  nfabd  2298  dvelimdc  2299  cleqf  2303  sbabel  2305  ralbidva  2431  rexbidva  2432  ralbidv  2435  rexbidv  2436  2ralbida  2454  2ralbidva  2455  nfraldya  2467  nfrexdya  2468  rgen2a  2484  ralimdva  2497  ralrimiv  2502  r19.21v  2507  ralrimdv  2509  reximdvai  2530  r19.23v  2539  rexlimiv  2541  rexlimdv  2546  r19.29af  2571  r19.29an  2572  r19.29a  2573  r19.32vr  2577  r19.37av  2582  r19.41v  2585  reean  2597  reeanv  2598  reubidva  2611  rmobidva  2616  cbvralf  2646  cbvrexf  2647  cbvreu  2650  cbvralv  2652  cbvrexv  2653  cbvreuv  2654  cbvrmov  2655  cbvralsv  2663  cbvrexsv  2664  sbralie  2665  cbvrab  2679  cbvrabv  2680  issetf  2688  ceqsalv  2711  ceqsralv  2712  ceqsexv  2720  ceqsex2  2721  ceqsex2v  2722  vtocld  2733  vtocl  2735  vtocl2  2736  vtocl3  2737  vtoclg  2741  vtocl2g  2745  vtoclga  2747  vtocl2gaf  2748  vtocl2ga  2749  vtocl3gaf  2750  vtocl3ga  2751  spcimdv  2765  spcimedv  2767  spcgv  2768  spcegv  2769  rspct  2777  rspc  2778  rspce  2779  rspcv  2780  rspcev  2784  rspc2v  2797  eqvincg  2804  eqvincf  2805  ceqsexgv  2809  elabgt  2820  elab  2823  elabg  2825  elab3g  2830  elrab3t  2834  elrab  2835  ralab2  2843  rexab2  2845  eqeu  2849  mosubt  2856  mo2icl  2858  mob2  2859  mob  2861  reu2  2867  reu3  2869  rmo4f  2877  nfcdeq  2901  sbcco  2925  sbcco2  2926  cbvsbcv  2933  sbcieg  2936  sbcie2g  2937  sbcied  2940  elrabsf  2942  sbcbidv  2962  sbcg  2973  sbc2iegf  2974  sbc2ie  2975  rmo2ilem  2993  rmo3  2995  csbeq2dv  3023  nfcsb1d  3028  nfcsbd  3031  csbiebt  3034  csbied  3041  csbie2t  3043  sbcnestg  3048  sbnfc2  3055  cbvralcsf  3057  cbvrexcsf  3058  cbvreucsf  3059  cbvrabcsf  3060  cbvralv2  3061  cbvrexv2  3062  dfss2f  3083  uniiunlem  3180  abn0m  3383  rabn0m  3385  rabeq0  3387  abeq0  3388  r19.3rmv  3448  r19.28mv  3450  r19.27mv  3454  raaanv  3465  sbss  3466  nfifd  3494  euabsn  3588  oprcl  3724  nfuni  3737  nfunid  3738  eluniab  3743  nfint  3776  elintab  3777  iineq2dv  3830  disjiun  3919  opabbidv  3989  nfopab  3991  cbvopab  3994  cbvopabv  3995  cbvopab1  3996  cbvopab2  3997  cbvopab1s  3998  cbvopab1v  3999  mpteq12f  4003  mpteq2dva  4013  cbvmptf  4017  cbvmpt  4018  zfrep6  4040  zfnuleu  4047  intexabim  4072  iinexgm  4074  repizf2  4081  bnd  4091  copsex2t  4162  copsex2g  4163  opelopabsb  4177  opelopabaf  4190  pofun  4229  frind  4269  reusv3  4376  alxfr  4377  rexxfrd  4379  ralxfrALT  4383  onintonm  4428  sucprcreg  4459  eunex  4471  tfis  4492  tfis2  4494  tfisi  4496  peano2  4504  findes  4512  omsinds  4530  opeliunxp  4589  opeliunxp2  4674  ralxpf  4680  rexxpf  4681  dfdmf  4727  dfrnf  4775  elrnmpt1  4785  intirr  4920  nfiotadw  5086  cbviota  5088  cbviotav  5089  sb8iota  5090  iota2d  5108  iota2  5109  dffun5r  5130  dffun6f  5131  dffun4f  5134  funco  5158  fun11  5185  imadif  5198  isarep1  5204  isarep2  5205  fun11iun  5381  fv3  5437  tz6.12f  5443  tz6.12c  5444  relelfvdm  5446  nfvres  5447  funimass4  5465  funfvdm2f  5479  fvmptss2  5489  fvmptdf  5501  fvmptdv  5502  fvmptt  5505  eqfnfv2f  5515  ralrnmpt  5555  rexrnmpt  5556  f1ompt  5564  ffnfv  5571  ffnfvf  5572  fmptco  5579  elabrex  5652  dff13f  5664  fliftfun  5690  cbvriota  5733  cbvriotav  5734  riota2  5745  riota5f  5747  acexmid  5766  nfoprab  5816  oprabbidv  5818  mpoeq123  5823  cbvoprab1  5836  cbvoprab2  5837  cbvoprab12  5838  cbvoprab12v  5839  cbvoprab3  5840  cbvoprab3v  5841  cbvmpox  5842  ralrnmpo  5878  ovmpodx  5890  ovmpodf  5895  ovmpodv  5896  ovi3  5900  ofrfval2  5991  abrexex2g  6011  opabex3d  6012  opabex3  6013  abrexex2  6015  dfoprab4f  6084  fmpox  6091  spc2ed  6123  cnvoprab  6124  f1od2  6125  opeliunxp2f  6128  tposoprab  6170  nfrecs  6197  tfri3  6257  nffrec  6286  eqerlem  6453  erovlem  6514  mptelixpg  6621  dom2lem  6659  xpf1o  6731  mapxpen  6735  nneneq  6744  findcard2  6776  findcard2s  6777  ac6sfi  6785  fiintim  6810  exmidomni  7007  fodjuomnilemdc  7009  ismkvnex  7022  mkvprop  7025  exmidfodomrlemr  7051  exmidfodomrlemrALT  7052  indpi  7143  prarloclem3step  7297  prmuloc2  7368  ltexprlemm  7401  caucvgprprlemaddq  7509  caucvgsrlemgt1  7596  suplocsrlem  7609  axpre-suploclemres  7702  nn0ind-raph  9161  uzind4s  9378  indstr  9381  supinfneg  9383  infsupneg  9384  lbzbi  9401  fzrevral  9878  frecuzrdgtcl  10178  frecuzrdgfunlem  10185  uzsinds  10208  seq3f1olemstep  10267  seq3f1olemp  10268  fimaxre2  10991  climeu  11058  nfsum1  11118  nfsum  11119  sumrbdclem  11138  summodclem2a  11143  zsumdc  11146  fsum3  11149  isumss  11153  isumss2  11155  fsum3cvg2  11156  fsumsplitf  11170  fsum2dlemstep  11196  fsum00  11224  fsumrelem  11233  mertenslem2  11298  nfcprod1  11316  nfcprod  11317  prodeq2  11319  prodrbdclem  11333  divalglemeunn  11607  divalglemeuneg  11609  zsupcllemstep  11627  bezoutlemnewy  11673  bezoutlemmain  11675  bezoutlemzz  11679  bezout  11688  prmind2  11790  oddpwdclemdvds  11837  oddpwdclemndvds  11838  exmidunben  11928  ctiunctlemfo  11941  ctiunct  11942  cnmpt11  12441  cnmpt21  12449  cnmptcom  12456  imasnopn  12457  mulcncf  12749  ellimc3apf  12787  limccnp2cntop  12804  ch2varv  12964  elab1  12979  elab2a  12980  elabg2  12981  cbvrald  12984  sumdc2  12995  bdsepnft  13074  bdsepnfALT  13076  bj-omssind  13122  bj-bdfindes  13136  bj-nn0suc0  13137  bj-nntrans  13138  bj-nnelirr  13140  bj-omtrans  13143  setindft  13152  bj-inf2vnlem3  13159  bj-inf2vnlem4  13160  bj-nn0sucALT  13165  bj-findis  13166  bj-findes  13168  strcollnft  13171  strcollnfALT  13173  sscoll2  13175  isomninnlem  13214  trilpolemeq1  13222