Theorem nfv 1574

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

Syntax hints:   F/wnf 1506

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 1495  ax-17 1572

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

This theorem is referenced by:  nfvd  1575  alexim  1691  19.37aiv  1721  sbiedv  1835  spimv  1857  spimev  1907  19.36aiv  1948  cbval2  1968  cbvex2  1969  cbval2v  1970  cbvex2v  1971  cbvald  1972  cbvaldva  1975  cbvexdva  1976  eeanv  1983  nfsbv  1998  sbco2h  2015  nfsbt  2027  sbnf2  2032  dfsb7a  2045  sbalyz  2050  sbco4lem  2057  sbco4  2058  dvelimALT  2061  eubidv  2085  sb8eu  2090  nfeudv  2092  nfeud  2093  nfeuv  2095  nfeu  2096  mobidv  2113  mo23  2119  sbmo  2137  mo4  2139  moimv  2144  moanimv  2153  bm1.1  2214  eqsb1lem  2332  eqsb1  2333  clelsb1  2334  clelsb2  2335  abbi  2343  abbidv  2347  cbvabv  2354  clelab  2355  nfcjust  2360  nfcv  2372  clelsb1f  2376  nfeqd  2387  nfeld  2388  nfabdw  2391  nfabd  2392  dvelimdc  2393  cleqf  2397  sbabel  2399  ralbidva  2526  rexbidva  2527  ralbidv  2530  rexbidv  2531  2ralbida  2551  2ralbidva  2552  nfraldya  2565  nfrexdya  2566  rgen2a  2584  ralimdva  2597  ralrimiv  2602  r19.21v  2607  ralrimdv  2609  reximdvai  2630  r19.23v  2640  rexlimiv  2642  rexlimdv  2647  r19.29af  2672  r19.29an  2673  r19.29a  2674  r19.32vr  2679  r19.37av  2684  r19.41v  2687  reean  2700  reeanv  2701  cbvrmow  2714  reubidva  2715  rmobidva  2720  cbvralf  2756  cbvrexf  2757  cbvreu  2763  cbvralv  2765  cbvrexv  2766  cbvreuv  2767  cbvrmov  2768  cbvralsv  2781  cbvrexsv  2782  sbralie  2783  cbvrab  2797  cbvrabv  2798  issetf  2807  ceqsalv  2830  ceqsralv  2831  ceqsexv  2839  ceqsex2  2841  ceqsex2v  2842  vtocld  2853  vtocl  2855  vtocl2  2856  vtocl3  2857  vtoclg  2861  vtocl2g  2865  vtoclga  2867  vtocl2gaf  2868  vtocl2ga  2869  vtocl3gaf  2870  vtocl3ga  2871  spcimdv  2887  spcimedv  2889  spcgv  2890  spcegv  2891  rspct  2900  rspc  2901  rspce  2902  rspcv  2903  rspcev  2907  rspc2v  2920  eqvincg  2927  eqvincf  2928  ceqsexgv  2932  elabgt  2944  elab  2947  elabg  2949  elab3g  2954  elrab3t  2958  elrab  2959  ralab2  2967  rexab2  2969  eqeu  2973  mosubt  2980  mo2icl  2982  mob2  2983  mob  2985  reu2  2991  reu3  2993  rmo4f  3001  nfcdeq  3025  sbcco  3050  sbcco2  3051  cbvsbcv  3058  sbcieg  3061  sbcie2g  3062  sbcied  3065  elrabsf  3067  sbcbidv  3087  sbcg  3098  sbc2iegf  3099  sbc2ie  3100  reu8nf  3110  rmo2ilem  3119  rmo3  3121  csbcow  3135  csbeq2dv  3150  nfcsb1d  3155  nfcsbd  3160  csbiebt  3164  csbied  3171  csbie2t  3173  sbcnestg  3178  sbnfc2  3185  cbvralcsf  3187  cbvrexcsf  3188  cbvreucsf  3189  cbvrabcsf  3190  cbvralv2  3191  cbvrexv2  3192  rspc2vd  3193  dfss2f  3215  uniiunlem  3313  abn0m  3517  rabn0m  3519  rabeq0  3521  abeq0  3522  r19.3rmv  3582  r19.28mv  3584  r19.27mv  3588  raaanv  3598  sbss  3599  nfifd  3630  euabsn  3736  oprcl  3881  nfuni  3894  nfunid  3895  eluniab  3900  nfint  3933  elintab  3934  iineq2dv  3987  disjiun  4078  opabbidv  4150  nfopab  4152  cbvopab  4155  cbvopabv  4156  cbvopab1  4157  cbvopab2  4158  cbvopab1s  4159  cbvopab1v  4160  mpteq12f  4164  mpteq2dva  4174  cbvmptf  4178  cbvmpt  4179  zfrep6  4201  zfnuleu  4208  intexabim  4236  iinexgm  4238  repizf2  4246  bnd  4256  copsex2t  4331  copsex2g  4332  opelopabsb  4348  opelopabaf  4362  pofun  4403  frind  4443  reusv3  4551  alxfr  4552  rexxfrd  4554  ralxfrALT  4558  onintonm  4609  sucprcreg  4641  eunex  4653  tfis  4675  tfis2  4677  tfisi  4679  peano2  4687  findes  4695  omsinds  4714  opeliunxp  4774  opeliunxp2  4862  ralxpf  4868  rexxpf  4869  dfdmf  4916  reldmm  4942  dfrnf  4965  elrnmpt1  4975  intirr  5115  nfiotadw  5281  cbviota  5283  cbviotav  5285  sb8iota  5286  iota2d  5305  iota2  5308  dffun5r  5330  dffun6f  5331  dffun4f  5334  funco  5358  fun11  5388  imadif  5401  isarep1  5407  isarep2  5408  fun11iun  5593  fv3  5650  tz6.12f  5656  tz6.12c  5657  relelfvdm  5659  nfvres  5663  funimass4  5684  funfvdm2f  5699  fvmptss2  5709  fvmptdf  5722  fvmptdv  5723  fvmptt  5726  eqfnfv2f  5736  ralrnmpt  5777  rexrnmpt  5778  f1ompt  5786  ffnfv  5793  ffnfvf  5794  fmptco  5801  elabrex  5881  elabrexg  5882  dff13f  5894  fliftfun  5920  cbvriota  5966  cbvriotav  5967  riota2  5978  riotaeqimp  5979  riota5f  5981  acexmid  6000  nfoprab  6056  oprabbidv  6058  mpoeq123  6063  cbvoprab1  6076  cbvoprab2  6077  cbvoprab12  6078  cbvoprab12v  6079  cbvoprab3  6080  cbvoprab3v  6081  cbvmpox  6082  ralrnmpo  6119  ovmpodx  6131  ovmpodf  6136  ovmpodv  6137  ovi3  6142  ofrfval2  6235  abrexex2g  6265  opabex3d  6266  opabex3  6267  abrexex2  6269  uchoice  6283  dfoprab4f  6339  fmpox  6346  spc2ed  6379  cnvoprab  6380  f1od2  6381  opeliunxp2f  6384  tposoprab  6426  nfrecs  6453  tfri3  6513  nffrec  6542  eqerlem  6711  erovlem  6774  mptelixpg  6881  dom2lem  6923  xpf1o  7005  mapxpen  7009  nneneq  7018  findcard2  7051  findcard2s  7052  ac6sfi  7060  fiintim  7093  opabfi  7100  exmidomni  7309  fodjuomnilemdc  7311  ismkvnex  7322  mkvprop  7325  exmidfodomrlemr  7380  exmidfodomrlemrALT  7381  cc3  7454  indpi  7529  prarloclem3step  7683  prmuloc2  7754  ltexprlemm  7787  caucvgprprlemaddq  7895  caucvgsrlemgt1  7982  suplocsrlem  7995  axpre-suploclemres  8088  nn0ind-raph  9564  uzind4s  9785  indstr  9788  supinfneg  9790  infsupneg  9791  lbzbi  9811  fzrevral  10301  zsupcllemstep  10449  frecuzrdgtcl  10634  frecuzrdgfunlem  10641  nninfinf  10665  uzsinds  10666  seq3f1olemstep  10736  seq3f1olemp  10737  wrd2ind  11255  reuccatpfxs1  11279  fimaxre2  11738  climeu  11807  nfsum1  11867  nfsum  11868  sumrbdclem  11888  summodclem2a  11892  zsumdc  11895  fsum3  11898  isumss  11902  isumss2  11904  fsum3cvg2  11905  fsumsplitf  11919  fsum2dlemstep  11945  fsum00  11973  fsumrelem  11982  mertenslem2  12047  nfcprod1  12065  nfcprod  12066  prodeq2  12068  prodrbdclem  12082  prodmodclem2a  12087  zproddc  12090  fprodseq  12094  fprodntrivap  12095  prodssdc  12100  fprodcl2lem  12116  fprod2dlemstep  12133  fprodsplitf  12143  fprodsplit1f  12145  fprodap0f  12147  fprodle  12151  divalglemeunn  12432  divalglemeuneg  12434  bezoutlemnewy  12517  bezoutlemmain  12519  bezoutlemzz  12523  bezout  12532  nnwofdc  12559  prmind2  12642  oddpwdclemdvds  12692  oddpwdclemndvds  12693  pcmpt  12866  pcmptdvds  12868  exmidunben  12997  ctiunctlemfo  13010  ctiunct  13011  ctiunctal  13012  dfgrp3mlem  13631  lss1d  14347  gsumfzfsumlemm  14551  cnmpt11  14957  cnmpt21  14965  cnmptcom  14972  imasnopn  14973  mulcncf  15282  ellimc3apf  15334  limccnp2cntop  15351  dvmptfsum  15399  lgseisenlem2  15750  gropd  15848  grstructd2dom  15849  ch2varv  16132  elab1  16147  elab2a  16148  elabg2  16149  cbvrald  16152  sumdc2  16163  bdsepnft  16250  bdsepnfALT  16252  bj-omssind  16298  bj-bdfindes  16312  bj-nn0suc0  16313  bj-nntrans  16314  bj-nnelirr  16316  bj-omtrans  16319  setindft  16328  bj-inf2vnlem3  16335  bj-inf2vnlem4  16336  bj-nn0sucALT  16341  bj-findis  16342  bj-findes  16344  strcollnft  16347  strcollnfALT  16349  pw1nct  16369  isomninnlem  16398  trilpolemeq1  16408  trirec0  16412  iswomninnlem  16417  ismkvnnlem  16420  nconstwlpolemgt0  16432