Theorem nfv 1539

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

Syntax hints:   F/wnf 1471

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 1460  ax-17 1537

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

This theorem is referenced by:  nfvd  1540  alexim  1656  19.37aiv  1686  sbiedv  1800  spimv  1822  spimev  1872  19.36aiv  1913  cbval2  1933  cbvex2  1934  cbval2v  1935  cbvex2v  1936  cbvald  1937  cbvaldva  1940  cbvexdva  1941  eeanv  1948  nfsbv  1963  sbco2h  1980  nfsbt  1992  sbnf2  1997  dfsb7a  2010  sbalyz  2015  sbco4lem  2022  sbco4  2023  dvelimALT  2026  eubidv  2050  sb8eu  2055  nfeudv  2057  nfeud  2058  nfeuv  2060  nfeu  2061  mobidv  2078  mo23  2083  sbmo  2101  mo4  2103  moimv  2108  moanimv  2117  bm1.1  2178  eqsb1lem  2296  eqsb1  2297  clelsb1  2298  clelsb2  2299  abbi  2307  abbidv  2311  cbvabv  2318  clelab  2319  nfcjust  2324  nfcv  2336  clelsb1f  2340  nfeqd  2351  nfeld  2352  nfabdw  2355  nfabd  2356  dvelimdc  2357  cleqf  2361  sbabel  2363  ralbidva  2490  rexbidva  2491  ralbidv  2494  rexbidv  2495  2ralbida  2515  2ralbidva  2516  nfraldya  2529  nfrexdya  2530  rgen2a  2548  ralimdva  2561  ralrimiv  2566  r19.21v  2571  ralrimdv  2573  reximdvai  2594  r19.23v  2603  rexlimiv  2605  rexlimdv  2610  r19.29af  2635  r19.29an  2636  r19.29a  2637  r19.32vr  2642  r19.37av  2647  r19.41v  2650  reean  2663  reeanv  2664  reubidva  2677  rmobidva  2682  cbvralf  2718  cbvrexf  2719  cbvreu  2724  cbvralv  2726  cbvrexv  2727  cbvreuv  2728  cbvrmov  2729  cbvralsv  2742  cbvrexsv  2743  sbralie  2744  cbvrab  2758  cbvrabv  2759  issetf  2767  ceqsalv  2790  ceqsralv  2791  ceqsexv  2799  ceqsex2  2800  ceqsex2v  2801  vtocld  2812  vtocl  2814  vtocl2  2815  vtocl3  2816  vtoclg  2820  vtocl2g  2824  vtoclga  2826  vtocl2gaf  2827  vtocl2ga  2828  vtocl3gaf  2829  vtocl3ga  2830  spcimdv  2844  spcimedv  2846  spcgv  2847  spcegv  2848  rspct  2857  rspc  2858  rspce  2859  rspcv  2860  rspcev  2864  rspc2v  2877  eqvincg  2884  eqvincf  2885  ceqsexgv  2889  elabgt  2901  elab  2904  elabg  2906  elab3g  2911  elrab3t  2915  elrab  2916  ralab2  2924  rexab2  2926  eqeu  2930  mosubt  2937  mo2icl  2939  mob2  2940  mob  2942  reu2  2948  reu3  2950  rmo4f  2958  nfcdeq  2982  sbcco  3007  sbcco2  3008  cbvsbcv  3015  sbcieg  3018  sbcie2g  3019  sbcied  3022  elrabsf  3024  sbcbidv  3044  sbcg  3055  sbc2iegf  3056  sbc2ie  3057  rmo2ilem  3075  rmo3  3077  csbcow  3091  csbeq2dv  3106  nfcsb1d  3111  nfcsbd  3116  csbiebt  3120  csbied  3127  csbie2t  3129  sbcnestg  3134  sbnfc2  3141  cbvralcsf  3143  cbvrexcsf  3144  cbvreucsf  3145  cbvrabcsf  3146  cbvralv2  3147  cbvrexv2  3148  rspc2vd  3149  dfss2f  3170  uniiunlem  3268  abn0m  3472  rabn0m  3474  rabeq0  3476  abeq0  3477  r19.3rmv  3537  r19.28mv  3539  r19.27mv  3543  raaanv  3553  sbss  3554  nfifd  3584  euabsn  3688  oprcl  3828  nfuni  3841  nfunid  3842  eluniab  3847  nfint  3880  elintab  3881  iineq2dv  3934  disjiun  4024  opabbidv  4095  nfopab  4097  cbvopab  4100  cbvopabv  4101  cbvopab1  4102  cbvopab2  4103  cbvopab1s  4104  cbvopab1v  4105  mpteq12f  4109  mpteq2dva  4119  cbvmptf  4123  cbvmpt  4124  zfrep6  4146  zfnuleu  4153  intexabim  4181  iinexgm  4183  repizf2  4191  bnd  4201  copsex2t  4274  copsex2g  4275  opelopabsb  4290  opelopabaf  4304  pofun  4343  frind  4383  reusv3  4491  alxfr  4492  rexxfrd  4494  ralxfrALT  4498  onintonm  4549  sucprcreg  4581  eunex  4593  tfis  4615  tfis2  4617  tfisi  4619  peano2  4627  findes  4635  omsinds  4654  opeliunxp  4714  opeliunxp2  4802  ralxpf  4808  rexxpf  4809  dfdmf  4855  dfrnf  4903  elrnmpt1  4913  intirr  5052  nfiotadw  5218  cbviota  5220  cbviotav  5221  sb8iota  5222  iota2d  5241  iota2  5244  dffun5r  5266  dffun6f  5267  dffun4f  5270  funco  5294  fun11  5321  imadif  5334  isarep1  5340  isarep2  5341  fun11iun  5521  fv3  5577  tz6.12f  5583  tz6.12c  5584  relelfvdm  5586  nfvres  5588  funimass4  5607  funfvdm2f  5622  fvmptss2  5632  fvmptdf  5645  fvmptdv  5646  fvmptt  5649  eqfnfv2f  5659  ralrnmpt  5700  rexrnmpt  5701  f1ompt  5709  ffnfv  5716  ffnfvf  5717  fmptco  5724  elabrex  5800  elabrexg  5801  dff13f  5813  fliftfun  5839  cbvriota  5884  cbvriotav  5885  riota2  5896  riota5f  5898  acexmid  5917  nfoprab  5970  oprabbidv  5972  mpoeq123  5977  cbvoprab1  5990  cbvoprab2  5991  cbvoprab12  5992  cbvoprab12v  5993  cbvoprab3  5994  cbvoprab3v  5995  cbvmpox  5996  ralrnmpo  6033  ovmpodx  6045  ovmpodf  6050  ovmpodv  6051  ovi3  6055  ofrfval2  6147  abrexex2g  6172  opabex3d  6173  opabex3  6174  abrexex2  6176  uchoice  6190  dfoprab4f  6246  fmpox  6253  spc2ed  6286  cnvoprab  6287  f1od2  6288  opeliunxp2f  6291  tposoprab  6333  nfrecs  6360  tfri3  6420  nffrec  6449  eqerlem  6618  erovlem  6681  mptelixpg  6788  dom2lem  6826  xpf1o  6900  mapxpen  6904  nneneq  6913  findcard2  6945  findcard2s  6946  ac6sfi  6954  fiintim  6985  opabfi  6992  exmidomni  7201  fodjuomnilemdc  7203  ismkvnex  7214  mkvprop  7217  exmidfodomrlemr  7262  exmidfodomrlemrALT  7263  cc3  7328  indpi  7402  prarloclem3step  7556  prmuloc2  7627  ltexprlemm  7660  caucvgprprlemaddq  7768  caucvgsrlemgt1  7855  suplocsrlem  7868  axpre-suploclemres  7961  nn0ind-raph  9434  uzind4s  9655  indstr  9658  supinfneg  9660  infsupneg  9661  lbzbi  9681  fzrevral  10171  frecuzrdgtcl  10483  frecuzrdgfunlem  10490  nninfinf  10514  uzsinds  10515  seq3f1olemstep  10585  seq3f1olemp  10586  fimaxre2  11370  climeu  11439  nfsum1  11499  nfsum  11500  sumrbdclem  11520  summodclem2a  11524  zsumdc  11527  fsum3  11530  isumss  11534  isumss2  11536  fsum3cvg2  11537  fsumsplitf  11551  fsum2dlemstep  11577  fsum00  11605  fsumrelem  11614  mertenslem2  11679  nfcprod1  11697  nfcprod  11698  prodeq2  11700  prodrbdclem  11714  prodmodclem2a  11719  zproddc  11722  fprodseq  11726  fprodntrivap  11727  prodssdc  11732  fprodcl2lem  11748  fprod2dlemstep  11765  fprodsplitf  11775  fprodsplit1f  11777  fprodap0f  11779  fprodle  11783  divalglemeunn  12062  divalglemeuneg  12064  zsupcllemstep  12082  bezoutlemnewy  12133  bezoutlemmain  12135  bezoutlemzz  12139  bezout  12148  nnwofdc  12175  prmind2  12258  oddpwdclemdvds  12308  oddpwdclemndvds  12309  pcmpt  12481  pcmptdvds  12483  exmidunben  12583  ctiunctlemfo  12596  ctiunct  12597  ctiunctal  12598  dfgrp3mlem  13170  lss1d  13879  gsumfzfsumlemm  14075  cnmpt11  14451  cnmpt21  14459  cnmptcom  14466  imasnopn  14467  mulcncf  14762  ellimc3apf  14814  limccnp2cntop  14831  lgseisenlem2  15187  ch2varv  15260  elab1  15275  elab2a  15276  elabg2  15277  cbvrald  15280  sumdc2  15291  bdsepnft  15379  bdsepnfALT  15381  bj-omssind  15427  bj-bdfindes  15441  bj-nn0suc0  15442  bj-nntrans  15443  bj-nnelirr  15445  bj-omtrans  15448  setindft  15457  bj-inf2vnlem3  15464  bj-inf2vnlem4  15465  bj-nn0sucALT  15470  bj-findis  15471  bj-findes  15473  strcollnft  15476  strcollnfALT  15478  pw1nct  15493  isomninnlem  15520  trilpolemeq1  15530  trirec0  15534  iswomninnlem  15539  ismkvnnlem  15542  nconstwlpolemgt0  15554