Theorem nfv 1473

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

Syntax hints:   F/wnf 1401

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

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

This theorem is referenced by:  nfvd  1474  alexim  1588  19.37aiv  1617  sbiedv  1726  spimv  1746  spimev  1796  19.36aiv  1836  cbval2  1851  cbvex2  1852  cbval2v  1853  cbvex2v  1854  cbvald  1855  cbvaldva  1858  cbvexdva  1859  eeanv  1862  sbco2h  1893  nfsbt  1905  sbnf2  1912  dfsb7a  1925  sbalyz  1930  sbco4lem  1937  sbco4  1938  dvelimALT  1941  eubidv  1963  sb8eu  1968  nfeudv  1970  nfeud  1971  nfeuv  1973  nfeu  1974  mobidv  1991  mo23  1996  sbmo  2014  mo4  2016  moimv  2021  moanimv  2030  bm1.1  2080  eqsb3lem  2197  eqsb3  2198  clelsb3  2199  clelsb4  2200  abbi  2208  abbidv  2212  cbvabv  2218  clelab  2219  nfcjust  2223  nfcv  2235  clelsb3f  2239  nfeqd  2250  nfeld  2251  nfabd  2254  dvelimdc  2255  cleqf  2259  sbabel  2261  ralbidva  2387  rexbidva  2388  ralbidv  2391  rexbidv  2392  2ralbida  2410  2ralbidva  2411  nfraldya  2423  nfrexdya  2424  rgen2a  2440  ralimdva  2453  ralrimiv  2457  r19.21v  2462  ralrimdv  2464  reximdvai  2485  r19.23v  2494  rexlimiv  2496  rexlimdv  2501  r19.29af  2523  r19.29an  2524  r19.29a  2525  r19.32vr  2529  r19.37av  2534  r19.41v  2537  reean  2549  reeanv  2550  reubidva  2563  rmobidva  2568  cbvralf  2598  cbvrexf  2599  cbvreu  2602  cbvralv  2604  cbvrexv  2605  cbvreuv  2606  cbvrmov  2607  cbvralsv  2615  cbvrexsv  2616  sbralie  2617  cbvrab  2631  cbvrabv  2632  issetf  2640  ceqsalv  2663  ceqsralv  2664  ceqsexv  2672  ceqsex2  2673  ceqsex2v  2674  vtocld  2685  vtocl  2687  vtocl2  2688  vtocl3  2689  vtoclg  2693  vtocl2g  2697  vtoclga  2699  vtocl2gaf  2700  vtocl2ga  2701  vtocl3gaf  2702  vtocl3ga  2703  spcimdv  2717  spcimedv  2719  spcgv  2720  spcegv  2721  rspct  2729  rspc  2730  rspce  2731  rspcv  2732  rspcev  2736  rspc2v  2748  eqvincg  2755  eqvincf  2756  ceqsexgv  2760  elabgt  2771  elab  2774  elabg  2775  elab3g  2780  elrab3t  2784  elrab  2785  ralab2  2793  rexab2  2795  eqeu  2799  mosubt  2806  mo2icl  2808  mob2  2809  mob  2811  reu2  2817  reu3  2819  rmo4f  2827  nfcdeq  2851  sbcco  2875  sbcco2  2876  cbvsbcv  2882  sbcieg  2885  sbcie2g  2886  sbcied  2889  elrabsf  2891  sbcbidv  2911  sbcg  2922  sbc2iegf  2923  sbc2ie  2924  rmo2ilem  2942  rmo3  2944  csbeq2dv  2970  nfcsb1d  2975  nfcsbd  2978  csbiebt  2981  csbied  2988  csbie2t  2990  sbcnestg  2995  sbnfc2  3002  cbvralcsf  3004  cbvrexcsf  3005  cbvreucsf  3006  cbvrabcsf  3007  cbvralv2  3008  cbvrexv2  3009  dfss2f  3030  uniiunlem  3124  abn0m  3327  rabn0m  3329  rabeq0  3331  abeq0  3332  r19.3rmv  3392  r19.28mv  3394  r19.27mv  3398  raaanv  3409  sbss  3410  nfifd  3438  euabsn  3532  oprcl  3668  nfuni  3681  nfunid  3682  eluniab  3687  nfint  3720  elintab  3721  iineq2dv  3774  disjiun  3862  opabbidv  3926  nfopab  3928  cbvopab  3931  cbvopabv  3932  cbvopab1  3933  cbvopab2  3934  cbvopab1s  3935  cbvopab1v  3936  mpteq12f  3940  mpteq2dva  3950  cbvmptf  3954  cbvmpt  3955  zfrep6  3977  zfnuleu  3984  intexabim  4009  iinexgm  4011  repizf2  4018  bnd  4028  copsex2t  4096  copsex2g  4097  opelopabsb  4111  opelopabaf  4124  pofun  4163  frind  4203  reusv3  4310  alxfr  4311  rexxfrd  4313  ralxfrALT  4317  onintonm  4362  sucprcreg  4393  eunex  4405  tfis  4426  tfis2  4428  tfisi  4430  peano2  4438  findes  4446  omsinds  4463  opeliunxp  4522  opeliunxp2  4607  ralxpf  4613  rexxpf  4614  dfdmf  4660  dfrnf  4708  elrnmpt1  4718  intirr  4851  nfiotadxy  5017  cbviota  5019  cbviotav  5020  sb8iota  5021  iota2d  5039  iota2  5040  dffun5r  5061  dffun6f  5062  dffun4f  5065  funco  5088  fun11  5115  imadif  5128  isarep1  5134  isarep2  5135  fun11iun  5309  fv3  5363  tz6.12f  5368  tz6.12c  5369  relelfvdm  5371  nfvres  5372  funimass4  5390  funfvdm2f  5404  fvmptss2  5414  fvmptdf  5426  fvmptdv  5427  fvmptt  5430  eqfnfv2f  5440  ralrnmpt  5480  rexrnmpt  5481  f1ompt  5489  ffnfv  5495  ffnfvf  5496  fmptco  5503  elabrex  5575  dff13f  5587  fliftfun  5613  cbvriota  5656  cbvriotav  5657  riota2  5668  riota5f  5670  acexmid  5689  nfoprab  5739  oprabbidv  5741  mpt2eq123  5746  cbvoprab1  5758  cbvoprab2  5759  cbvoprab12  5760  cbvoprab12v  5761  cbvoprab3  5762  cbvoprab3v  5763  cbvmpt2x  5764  ralrnmpt2  5797  ovmpt2dx  5809  ovmpt2df  5814  ovmpt2dv  5815  ovi3  5819  ofrfval2  5909  abrexex2g  5929  opabex3d  5930  opabex3  5931  abrexex2  5933  dfoprab4f  6001  fmpt2x  6008  spc2ed  6036  cnvoprab  6037  f1od2  6038  opeliunxp2f  6041  tposoprab  6083  nfrecs  6110  tfri3  6170  nffrec  6199  eqerlem  6363  erovlem  6424  mptelixpg  6531  dom2lem  6569  xpf1o  6640  mapxpen  6644  nneneq  6653  findcard2  6685  findcard2s  6686  ac6sfi  6694  fiintim  6719  exmidomni  6885  fodjuomnilemdc  6887  mkvprop  6901  exmidfodomrlemr  6925  exmidfodomrlemrALT  6926  indpi  6998  prarloclem3step  7152  prmuloc2  7223  ltexprlemm  7256  caucvgprprlemaddq  7364  caucvgsrlemgt1  7437  nn0ind-raph  8962  uzind4s  9177  indstr  9180  supinfneg  9182  infsupneg  9183  lbzbi  9200  fzrevral  9668  frecuzrdgtcl  9968  frecuzrdgfunlem  9975  uzsinds  9997  seq3f1olemstep  10051  seq3f1olemp  10052  fimaxre2  10773  climeu  10839  nfsum1  10899  nfsum  10900  sumrbdclem  10919  summodclem2a  10924  zsumdc  10927  fsum3  10930  isumss  10934  isumss2  10936  fsum3cvg2  10937  fsumsplitf  10951  fsum2dlemstep  10977  fsum00  11005  fsumrelem  11014  mertenslem2  11079  divalglemeunn  11348  divalglemeuneg  11350  zsupcllemstep  11368  bezoutlemnewy  11412  bezoutlemmain  11414  bezoutlemzz  11418  bezout  11427  prmind2  11529  oddpwdclemdvds  11575  oddpwdclemndvds  11576  cnmpt11  12105  mulcncf  12354  ch2varv  12377  elab1  12391  elab2a  12392  elabg2  12393  cbvrald  12396  sumdc2  12407  bdsepnft  12486  bdsepnfALT  12488  bj-omssind  12538  bj-bdfindes  12552  bj-nn0suc0  12553  bj-nntrans  12554  bj-nnelirr  12556  bj-omtrans  12559  setindft  12568  bj-inf2vnlem3  12575  bj-inf2vnlem4  12576  bj-nn0sucALT  12581  bj-findis  12582  bj-findes  12584  strcollnft  12587  strcollnfALT  12589  sscoll2  12591