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  3174  uniiunlem  3272  abn0m  3476  rabn0m  3478  rabeq0  3480  abeq0  3481  r19.3rmv  3541  r19.28mv  3543  r19.27mv  3547  raaanv  3557  sbss  3558  nfifd  3588  euabsn  3692  oprcl  3832  nfuni  3845  nfunid  3846  eluniab  3851  nfint  3884  elintab  3885  iineq2dv  3938  disjiun  4028  opabbidv  4099  nfopab  4101  cbvopab  4104  cbvopabv  4105  cbvopab1  4106  cbvopab2  4107  cbvopab1s  4108  cbvopab1v  4109  mpteq12f  4113  mpteq2dva  4123  cbvmptf  4127  cbvmpt  4128  zfrep6  4150  zfnuleu  4157  intexabim  4185  iinexgm  4187  repizf2  4195  bnd  4205  copsex2t  4278  copsex2g  4279  opelopabsb  4294  opelopabaf  4308  pofun  4347  frind  4387  reusv3  4495  alxfr  4496  rexxfrd  4498  ralxfrALT  4502  onintonm  4553  sucprcreg  4585  eunex  4597  tfis  4619  tfis2  4621  tfisi  4623  peano2  4631  findes  4639  omsinds  4658  opeliunxp  4718  opeliunxp2  4806  ralxpf  4812  rexxpf  4813  dfdmf  4859  dfrnf  4907  elrnmpt1  4917  intirr  5056  nfiotadw  5222  cbviota  5224  cbviotav  5225  sb8iota  5226  iota2d  5245  iota2  5248  dffun5r  5270  dffun6f  5271  dffun4f  5274  funco  5298  fun11  5325  imadif  5338  isarep1  5344  isarep2  5345  fun11iun  5525  fv3  5581  tz6.12f  5587  tz6.12c  5588  relelfvdm  5590  nfvres  5592  funimass4  5611  funfvdm2f  5626  fvmptss2  5636  fvmptdf  5649  fvmptdv  5650  fvmptt  5653  eqfnfv2f  5663  ralrnmpt  5704  rexrnmpt  5705  f1ompt  5713  ffnfv  5720  ffnfvf  5721  fmptco  5728  elabrex  5804  elabrexg  5805  dff13f  5817  fliftfun  5843  cbvriota  5888  cbvriotav  5889  riota2  5900  riota5f  5902  acexmid  5921  nfoprab  5974  oprabbidv  5976  mpoeq123  5981  cbvoprab1  5994  cbvoprab2  5995  cbvoprab12  5996  cbvoprab12v  5997  cbvoprab3  5998  cbvoprab3v  5999  cbvmpox  6000  ralrnmpo  6037  ovmpodx  6049  ovmpodf  6054  ovmpodv  6055  ovi3  6060  ofrfval2  6152  abrexex2g  6177  opabex3d  6178  opabex3  6179  abrexex2  6181  uchoice  6195  dfoprab4f  6251  fmpox  6258  spc2ed  6291  cnvoprab  6292  f1od2  6293  opeliunxp2f  6296  tposoprab  6338  nfrecs  6365  tfri3  6425  nffrec  6454  eqerlem  6623  erovlem  6686  mptelixpg  6793  dom2lem  6831  xpf1o  6905  mapxpen  6909  nneneq  6918  findcard2  6950  findcard2s  6951  ac6sfi  6959  fiintim  6992  opabfi  6999  exmidomni  7208  fodjuomnilemdc  7210  ismkvnex  7221  mkvprop  7224  exmidfodomrlemr  7269  exmidfodomrlemrALT  7270  cc3  7335  indpi  7409  prarloclem3step  7563  prmuloc2  7634  ltexprlemm  7667  caucvgprprlemaddq  7775  caucvgsrlemgt1  7862  suplocsrlem  7875  axpre-suploclemres  7968  nn0ind-raph  9443  uzind4s  9664  indstr  9667  supinfneg  9669  infsupneg  9670  lbzbi  9690  fzrevral  10180  zsupcllemstep  10319  frecuzrdgtcl  10504  frecuzrdgfunlem  10511  nninfinf  10535  uzsinds  10536  seq3f1olemstep  10606  seq3f1olemp  10607  fimaxre2  11392  climeu  11461  nfsum1  11521  nfsum  11522  sumrbdclem  11542  summodclem2a  11546  zsumdc  11549  fsum3  11552  isumss  11556  isumss2  11558  fsum3cvg2  11559  fsumsplitf  11573  fsum2dlemstep  11599  fsum00  11627  fsumrelem  11636  mertenslem2  11701  nfcprod1  11719  nfcprod  11720  prodeq2  11722  prodrbdclem  11736  prodmodclem2a  11741  zproddc  11744  fprodseq  11748  fprodntrivap  11749  prodssdc  11754  fprodcl2lem  11770  fprod2dlemstep  11787  fprodsplitf  11797  fprodsplit1f  11799  fprodap0f  11801  fprodle  11805  divalglemeunn  12086  divalglemeuneg  12088  bezoutlemnewy  12163  bezoutlemmain  12165  bezoutlemzz  12169  bezout  12178  nnwofdc  12205  prmind2  12288  oddpwdclemdvds  12338  oddpwdclemndvds  12339  pcmpt  12512  pcmptdvds  12514  exmidunben  12643  ctiunctlemfo  12656  ctiunct  12657  ctiunctal  12658  dfgrp3mlem  13230  lss1d  13939  gsumfzfsumlemm  14143  cnmpt11  14519  cnmpt21  14527  cnmptcom  14534  imasnopn  14535  mulcncf  14844  ellimc3apf  14896  limccnp2cntop  14913  dvmptfsum  14961  lgseisenlem2  15312  ch2varv  15414  elab1  15429  elab2a  15430  elabg2  15431  cbvrald  15434  sumdc2  15445  bdsepnft  15533  bdsepnfALT  15535  bj-omssind  15581  bj-bdfindes  15595  bj-nn0suc0  15596  bj-nntrans  15597  bj-nnelirr  15599  bj-omtrans  15602  setindft  15611  bj-inf2vnlem3  15618  bj-inf2vnlem4  15619  bj-nn0sucALT  15624  bj-findis  15625  bj-findes  15627  strcollnft  15630  strcollnfALT  15632  pw1nct  15647  isomninnlem  15674  trilpolemeq1  15684  trirec0  15688  iswomninnlem  15693  ismkvnnlem  15696  nconstwlpolemgt0  15708