Theorem nfv 1461

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

Syntax hints:   F/wnf 1389

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-gen 1378  ax-17 1459

This theorem depends on definitions:  df-bi 115  df-nf 1390

This theorem is referenced by:  nfvd  1462  alexim  1576  19.37aiv  1605  sbiedv  1712  spimv  1732  spimev  1782  19.36aiv  1822  cbval2  1837  cbvex2  1838  cbval2v  1839  cbvex2v  1840  cbvald  1841  cbvaldva  1844  cbvexdva  1845  eeanv  1848  sbco2h  1879  nfsbt  1891  sbnf2  1898  dfsb7a  1911  sbalyz  1916  sbco4lem  1923  sbco4  1924  dvelimALT  1927  eubidv  1949  sb8eu  1954  nfeudv  1956  nfeud  1957  nfeuv  1959  nfeu  1960  mobidv  1977  mo23  1982  sbmo  2000  mo4  2002  moimv  2007  moanimv  2016  bm1.1  2066  eqsb3lem  2181  eqsb3  2182  clelsb3  2183  clelsb4  2184  abbi  2192  abbidv  2196  cbvabv  2202  clelab  2203  nfcjust  2207  nfcv  2219  nfeqd  2233  nfeld  2234  nfabd  2237  dvelimdc  2238  cleqf  2242  sbabel  2244  ralbidva  2364  rexbidva  2365  ralbidv  2368  rexbidv  2369  2ralbida  2387  2ralbidva  2388  nfraldya  2400  nfrexdya  2401  rgen2a  2417  ralimdva  2429  ralrimiv  2433  r19.21v  2438  ralrimdv  2440  reximdvai  2461  r19.23v  2469  rexlimiv  2471  rexlimdv  2476  r19.29af  2497  r19.29a  2498  r19.32vr  2502  r19.37av  2507  r19.41v  2510  reean  2522  reeanv  2523  reubidva  2536  rmobidva  2541  cbvralf  2571  cbvrexf  2572  cbvreu  2575  cbvralv  2577  cbvrexv  2578  cbvreuv  2579  cbvrmov  2580  cbvralsv  2588  cbvrexsv  2589  sbralie  2590  cbvrab  2599  cbvrabv  2600  issetf  2606  ceqsalv  2629  ceqsralv  2630  ceqsexv  2638  ceqsex2  2639  ceqsex2v  2640  vtocld  2651  vtocl  2653  vtocl2  2654  vtocl3  2655  vtoclg  2658  vtocl2g  2662  vtoclga  2664  vtocl2gaf  2665  vtocl2ga  2666  vtocl3gaf  2667  vtocl3ga  2668  spcimdv  2682  spcimedv  2684  spcgv  2685  spcegv  2686  rspct  2694  rspc  2695  rspce  2696  rspcv  2697  rspcev  2701  rspc2v  2713  eqvincg  2719  eqvincf  2720  ceqsexgv  2724  elabgt  2735  elab  2738  elabg  2739  elab3g  2744  elrab3t  2748  elrab  2749  ralab2  2756  rexab2  2758  eqeu  2762  mosubt  2769  mo2icl  2771  mob2  2772  mob  2774  reu2  2780  reu3  2782  nfcdeq  2812  sbcco  2836  sbcco2  2837  cbvsbcv  2843  sbcieg  2846  sbcie2g  2847  sbcied  2850  elrabsf  2852  sbcbidv  2872  sbcg  2883  sbc2iegf  2884  sbc2ie  2885  rmo2ilem  2903  rmo3  2905  csbeq2dv  2931  nfcsb1d  2936  nfcsbd  2939  csbiebt  2942  csbied  2948  csbie2t  2950  sbcnestg  2955  sbnfc2  2962  cbvralcsf  2964  cbvrexcsf  2965  cbvreucsf  2966  cbvrabcsf  2967  cbvralv2  2968  cbvrexv2  2969  dfss2f  2990  uniiunlem  3082  rabn0m  3272  rabeq0  3274  abeq0  3275  r19.3rmv  3332  r19.28mv  3334  r19.27mv  3337  raaanv  3348  sbss  3349  nfifd  3376  euabsn  3462  oprcl  3594  nfuni  3607  nfunid  3608  eluniab  3613  nfint  3646  elintab  3647  iineq2dv  3700  opabbidv  3844  nfopab  3846  cbvopab  3849  cbvopabv  3850  cbvopab1  3851  cbvopab2  3852  cbvopab1s  3853  cbvopab1v  3854  mpteq12f  3858  mpteq2dva  3868  cbvmpt  3872  zfrep6  3895  zfnuleu  3902  intexabim  3927  iinexgm  3929  repizf2  3936  bnd  3946  copsex2t  4000  copsex2g  4001  opelopabsb  4015  opelopabaf  4028  pofun  4067  frind  4107  reusv3  4210  alxfr  4211  rexxfrd  4213  ralxfrALT  4217  onintonm  4261  sucprcreg  4292  eunex  4304  tfis  4324  tfis2  4326  tfisi  4328  peano2  4336  findes  4344  opeliunxp  4413  opeliunxp2  4494  ralxpf  4500  rexxpf  4501  dfdmf  4546  dfrnf  4593  elrnmpt1  4603  intirr  4731  nfiotadxy  4890  cbviota  4892  cbviotav  4893  sb8iota  4894  iota2d  4912  iota2  4913  dffun5r  4934  dffun6f  4935  dffun4f  4938  funco  4960  fun11  4986  imadif  4999  isarep1  5005  isarep2  5006  fun11iun  5167  fv3  5218  tz6.12f  5223  tz6.12c  5224  relelfvdm  5226  nfvres  5227  funimass4  5245  funfvdm2f  5259  fvmptss2  5268  fvmptdf  5279  fvmptdv  5280  fvmptt  5283  eqfnfv2f  5290  ralrnmpt  5330  rexrnmpt  5331  f1ompt  5341  ffnfv  5344  ffnfvf  5345  fmptco  5351  elabrex  5418  dff13f  5430  fliftfun  5456  cbvriota  5498  cbvriotav  5499  riota2  5510  riota5f  5512  acexmid  5531  nfoprab  5577  oprabbidv  5579  mpt2eq123  5584  cbvoprab1  5596  cbvoprab2  5597  cbvoprab12  5598  cbvoprab12v  5599  cbvoprab3  5600  cbvoprab3v  5601  cbvmpt2x  5602  ralrnmpt2  5635  ovmpt2dx  5647  ovmpt2df  5652  ovmpt2dv  5653  ovi3  5657  ofrfval2  5747  abrexex2g  5767  opabex3d  5768  opabex3  5769  abrexex2  5771  dfoprab4f  5839  fmpt2x  5846  spc2ed  5874  cnvoprab  5875  f1od2  5876  tposoprab  5918  nfrecs  5945  tfri3  5976  nffrec  6005  eqerlem  6160  erovlem  6221  dom2lem  6275  nneneq  6343  findcard2  6373  findcard2s  6374  ac6sfi  6379  indpi  6532  prarloclem3step  6686  prmuloc2  6757  ltexprlemm  6790  caucvgprprlemaddq  6898  caucvgsrlemgt1  6971  nn0ind-raph  8464  uzind4s  8678  indstr  8681  supinfneg  8683  infsupneg  8684  lbzbi  8701  fzrevral  9122  frecuzrdgfn  9414  uzsinds  9428  fimaxre2  10109  climeu  10135  divalglemeunn  10321  divalglemeuneg  10323  zsupcllemstep  10341  bezoutlemnewy  10385  bezoutlemmain  10387  bezoutlemzz  10391  bezout  10400  prmind2  10502  oddpwdclemdvds  10548  oddpwdclemndvds  10549  ch2varv  10579  elab1  10593  elab2a  10594  elabg2  10595  cbvrald  10598  bdsepnft  10678  bdsepnfALT  10680  bj-omssind  10730  bj-bdfindes  10744  bj-nn0suc0  10745  bj-nntrans  10746  bj-nnelirr  10748  bj-omtrans  10751  setindft  10760  bj-inf2vnlem3  10767  bj-inf2vnlem4  10768  bj-nn0sucALT  10773  bj-findis  10774  bj-findes  10776  strcollnft  10779  strcollnfALT  10781  sscoll2  10783