Theorem nfv 1542

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

Syntax hints:   F/wnf 1474

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 1463  ax-17 1540

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

This theorem is referenced by:  nfvd  1543  alexim  1659  19.37aiv  1689  sbiedv  1803  spimv  1825  spimev  1875  19.36aiv  1916  cbval2  1936  cbvex2  1937  cbval2v  1938  cbvex2v  1939  cbvald  1940  cbvaldva  1943  cbvexdva  1944  eeanv  1951  nfsbv  1966  sbco2h  1983  nfsbt  1995  sbnf2  2000  dfsb7a  2013  sbalyz  2018  sbco4lem  2025  sbco4  2026  dvelimALT  2029  eubidv  2053  sb8eu  2058  nfeudv  2060  nfeud  2061  nfeuv  2063  nfeu  2064  mobidv  2081  mo23  2086  sbmo  2104  mo4  2106  moimv  2111  moanimv  2120  bm1.1  2181  eqsb1lem  2299  eqsb1  2300  clelsb1  2301  clelsb2  2302  abbi  2310  abbidv  2314  cbvabv  2321  clelab  2322  nfcjust  2327  nfcv  2339  clelsb1f  2343  nfeqd  2354  nfeld  2355  nfabdw  2358  nfabd  2359  dvelimdc  2360  cleqf  2364  sbabel  2366  ralbidva  2493  rexbidva  2494  ralbidv  2497  rexbidv  2498  2ralbida  2518  2ralbidva  2519  nfraldya  2532  nfrexdya  2533  rgen2a  2551  ralimdva  2564  ralrimiv  2569  r19.21v  2574  ralrimdv  2576  reximdvai  2597  r19.23v  2606  rexlimiv  2608  rexlimdv  2613  r19.29af  2638  r19.29an  2639  r19.29a  2640  r19.32vr  2645  r19.37av  2650  r19.41v  2653  reean  2666  reeanv  2667  reubidva  2680  rmobidva  2685  cbvralf  2721  cbvrexf  2722  cbvreu  2727  cbvralv  2729  cbvrexv  2730  cbvreuv  2731  cbvrmov  2732  cbvralsv  2745  cbvrexsv  2746  sbralie  2747  cbvrab  2761  cbvrabv  2762  issetf  2770  ceqsalv  2793  ceqsralv  2794  ceqsexv  2802  ceqsex2  2804  ceqsex2v  2805  vtocld  2816  vtocl  2818  vtocl2  2819  vtocl3  2820  vtoclg  2824  vtocl2g  2828  vtoclga  2830  vtocl2gaf  2831  vtocl2ga  2832  vtocl3gaf  2833  vtocl3ga  2834  spcimdv  2848  spcimedv  2850  spcgv  2851  spcegv  2852  rspct  2861  rspc  2862  rspce  2863  rspcv  2864  rspcev  2868  rspc2v  2881  eqvincg  2888  eqvincf  2889  ceqsexgv  2893  elabgt  2905  elab  2908  elabg  2910  elab3g  2915  elrab3t  2919  elrab  2920  ralab2  2928  rexab2  2930  eqeu  2934  mosubt  2941  mo2icl  2943  mob2  2944  mob  2946  reu2  2952  reu3  2954  rmo4f  2962  nfcdeq  2986  sbcco  3011  sbcco2  3012  cbvsbcv  3019  sbcieg  3022  sbcie2g  3023  sbcied  3026  elrabsf  3028  sbcbidv  3048  sbcg  3059  sbc2iegf  3060  sbc2ie  3061  rmo2ilem  3079  rmo3  3081  csbcow  3095  csbeq2dv  3110  nfcsb1d  3115  nfcsbd  3120  csbiebt  3124  csbied  3131  csbie2t  3133  sbcnestg  3138  sbnfc2  3145  cbvralcsf  3147  cbvrexcsf  3148  cbvreucsf  3149  cbvrabcsf  3150  cbvralv2  3151  cbvrexv2  3152  rspc2vd  3153  dfss2f  3175  uniiunlem  3273  abn0m  3477  rabn0m  3479  rabeq0  3481  abeq0  3482  r19.3rmv  3542  r19.28mv  3544  r19.27mv  3548  raaanv  3558  sbss  3559  nfifd  3589  euabsn  3693  oprcl  3833  nfuni  3846  nfunid  3847  eluniab  3852  nfint  3885  elintab  3886  iineq2dv  3939  disjiun  4029  opabbidv  4100  nfopab  4102  cbvopab  4105  cbvopabv  4106  cbvopab1  4107  cbvopab2  4108  cbvopab1s  4109  cbvopab1v  4110  mpteq12f  4114  mpteq2dva  4124  cbvmptf  4128  cbvmpt  4129  zfrep6  4151  zfnuleu  4158  intexabim  4186  iinexgm  4188  repizf2  4196  bnd  4206  copsex2t  4279  copsex2g  4280  opelopabsb  4295  opelopabaf  4309  pofun  4348  frind  4388  reusv3  4496  alxfr  4497  rexxfrd  4499  ralxfrALT  4503  onintonm  4554  sucprcreg  4586  eunex  4598  tfis  4620  tfis2  4622  tfisi  4624  peano2  4632  findes  4640  omsinds  4659  opeliunxp  4719  opeliunxp2  4807  ralxpf  4813  rexxpf  4814  dfdmf  4860  dfrnf  4908  elrnmpt1  4918  intirr  5057  nfiotadw  5223  cbviota  5225  cbviotav  5226  sb8iota  5227  iota2d  5246  iota2  5249  dffun5r  5271  dffun6f  5272  dffun4f  5275  funco  5299  fun11  5326  imadif  5339  isarep1  5345  isarep2  5346  fun11iun  5528  fv3  5584  tz6.12f  5590  tz6.12c  5591  relelfvdm  5593  nfvres  5595  funimass4  5614  funfvdm2f  5629  fvmptss2  5639  fvmptdf  5652  fvmptdv  5653  fvmptt  5656  eqfnfv2f  5666  ralrnmpt  5707  rexrnmpt  5708  f1ompt  5716  ffnfv  5723  ffnfvf  5724  fmptco  5731  elabrex  5807  elabrexg  5808  dff13f  5820  fliftfun  5846  cbvriota  5891  cbvriotav  5892  riota2  5903  riota5f  5905  acexmid  5924  nfoprab  5978  oprabbidv  5980  mpoeq123  5985  cbvoprab1  5998  cbvoprab2  5999  cbvoprab12  6000  cbvoprab12v  6001  cbvoprab3  6002  cbvoprab3v  6003  cbvmpox  6004  ralrnmpo  6041  ovmpodx  6053  ovmpodf  6058  ovmpodv  6059  ovi3  6064  ofrfval2  6156  abrexex2g  6186  opabex3d  6187  opabex3  6188  abrexex2  6190  uchoice  6204  dfoprab4f  6260  fmpox  6267  spc2ed  6300  cnvoprab  6301  f1od2  6302  opeliunxp2f  6305  tposoprab  6347  nfrecs  6374  tfri3  6434  nffrec  6463  eqerlem  6632  erovlem  6695  mptelixpg  6802  dom2lem  6840  xpf1o  6914  mapxpen  6918  nneneq  6927  findcard2  6959  findcard2s  6960  ac6sfi  6968  fiintim  7001  opabfi  7008  exmidomni  7217  fodjuomnilemdc  7219  ismkvnex  7230  mkvprop  7233  exmidfodomrlemr  7281  exmidfodomrlemrALT  7282  cc3  7351  indpi  7426  prarloclem3step  7580  prmuloc2  7651  ltexprlemm  7684  caucvgprprlemaddq  7792  caucvgsrlemgt1  7879  suplocsrlem  7892  axpre-suploclemres  7985  nn0ind-raph  9460  uzind4s  9681  indstr  9684  supinfneg  9686  infsupneg  9687  lbzbi  9707  fzrevral  10197  zsupcllemstep  10336  frecuzrdgtcl  10521  frecuzrdgfunlem  10528  nninfinf  10552  uzsinds  10553  seq3f1olemstep  10623  seq3f1olemp  10624  fimaxre2  11409  climeu  11478  nfsum1  11538  nfsum  11539  sumrbdclem  11559  summodclem2a  11563  zsumdc  11566  fsum3  11569  isumss  11573  isumss2  11575  fsum3cvg2  11576  fsumsplitf  11590  fsum2dlemstep  11616  fsum00  11644  fsumrelem  11653  mertenslem2  11718  nfcprod1  11736  nfcprod  11737  prodeq2  11739  prodrbdclem  11753  prodmodclem2a  11758  zproddc  11761  fprodseq  11765  fprodntrivap  11766  prodssdc  11771  fprodcl2lem  11787  fprod2dlemstep  11804  fprodsplitf  11814  fprodsplit1f  11816  fprodap0f  11818  fprodle  11822  divalglemeunn  12103  divalglemeuneg  12105  bezoutlemnewy  12188  bezoutlemmain  12190  bezoutlemzz  12194  bezout  12203  nnwofdc  12230  prmind2  12313  oddpwdclemdvds  12363  oddpwdclemndvds  12364  pcmpt  12537  pcmptdvds  12539  exmidunben  12668  ctiunctlemfo  12681  ctiunct  12682  ctiunctal  12683  dfgrp3mlem  13300  lss1d  14015  gsumfzfsumlemm  14219  cnmpt11  14603  cnmpt21  14611  cnmptcom  14618  imasnopn  14619  mulcncf  14928  ellimc3apf  14980  limccnp2cntop  14997  dvmptfsum  15045  lgseisenlem2  15396  ch2varv  15498  elab1  15513  elab2a  15514  elabg2  15515  cbvrald  15518  sumdc2  15529  bdsepnft  15617  bdsepnfALT  15619  bj-omssind  15665  bj-bdfindes  15679  bj-nn0suc0  15680  bj-nntrans  15681  bj-nnelirr  15683  bj-omtrans  15686  setindft  15695  bj-inf2vnlem3  15702  bj-inf2vnlem4  15703  bj-nn0sucALT  15708  bj-findis  15709  bj-findes  15711  strcollnft  15714  strcollnfALT  15716  pw1nct  15734  isomninnlem  15761  trilpolemeq1  15771  trirec0  15775  iswomninnlem  15780  ismkvnnlem  15783  nconstwlpolemgt0  15795