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  5595  fv3  5652  tz6.12f  5658  tz6.12c  5659  relelfvdm  5661  nfvres  5665  funimass4  5686  funfvdm2f  5701  fvmptss2  5711  fvmptdf  5724  fvmptdv  5725  fvmptt  5728  eqfnfv2f  5738  ralrnmpt  5779  rexrnmpt  5780  f1ompt  5788  ffnfv  5795  ffnfvf  5796  fmptco  5803  elabrex  5887  elabrexg  5888  dff13f  5900  fliftfun  5926  cbvriota  5972  cbvriotav  5973  riota2  5984  riotaeqimp  5985  riota5f  5987  acexmid  6006  nfoprab  6062  oprabbidv  6064  mpoeq123  6069  cbvoprab1  6082  cbvoprab2  6083  cbvoprab12  6084  cbvoprab12v  6085  cbvoprab3  6086  cbvoprab3v  6087  cbvmpox  6088  ralrnmpo  6125  ovmpodx  6137  ovmpodf  6142  ovmpodv  6143  ovi3  6148  ofrfval2  6241  abrexex2g  6271  opabex3d  6272  opabex3  6273  abrexex2  6275  uchoice  6289  dfoprab4f  6345  fmpox  6352  spc2ed  6385  cnvoprab  6386  f1od2  6387  opeliunxp2f  6390  tposoprab  6432  nfrecs  6459  tfri3  6519  nffrec  6548  eqerlem  6719  erovlem  6782  mptelixpg  6889  dom2lem  6931  xpf1o  7013  mapxpen  7017  nneneq  7026  findcard2  7059  findcard2s  7060  ac6sfi  7068  fiintim  7104  opabfi  7111  exmidomni  7320  fodjuomnilemdc  7322  ismkvnex  7333  mkvprop  7336  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  cc3  7465  indpi  7540  prarloclem3step  7694  prmuloc2  7765  ltexprlemm  7798  caucvgprprlemaddq  7906  caucvgsrlemgt1  7993  suplocsrlem  8006  axpre-suploclemres  8099  nn0ind-raph  9575  uzind4s  9797  indstr  9800  supinfneg  9802  infsupneg  9803  lbzbi  9823  fzrevral  10313  zsupcllemstep  10461  frecuzrdgtcl  10646  frecuzrdgfunlem  10653  nninfinf  10677  uzsinds  10678  seq3f1olemstep  10748  seq3f1olemp  10749  wrd2ind  11271  reuccatpfxs1  11295  fimaxre2  11754  climeu  11823  nfsum1  11883  nfsum  11884  sumrbdclem  11904  summodclem2a  11908  zsumdc  11911  fsum3  11914  isumss  11918  isumss2  11920  fsum3cvg2  11921  fsumsplitf  11935  fsum2dlemstep  11961  fsum00  11989  fsumrelem  11998  mertenslem2  12063  nfcprod1  12081  nfcprod  12082  prodeq2  12084  prodrbdclem  12098  prodmodclem2a  12103  zproddc  12106  fprodseq  12110  fprodntrivap  12111  prodssdc  12116  fprodcl2lem  12132  fprod2dlemstep  12149  fprodsplitf  12159  fprodsplit1f  12161  fprodap0f  12163  fprodle  12167  divalglemeunn  12448  divalglemeuneg  12450  bezoutlemnewy  12533  bezoutlemmain  12535  bezoutlemzz  12539  bezout  12548  nnwofdc  12575  prmind2  12658  oddpwdclemdvds  12708  oddpwdclemndvds  12709  pcmpt  12882  pcmptdvds  12884  exmidunben  13013  ctiunctlemfo  13026  ctiunct  13027  ctiunctal  13028  dfgrp3mlem  13647  lss1d  14363  gsumfzfsumlemm  14567  cnmpt11  14973  cnmpt21  14981  cnmptcom  14988  imasnopn  14989  mulcncf  15298  ellimc3apf  15350  limccnp2cntop  15367  dvmptfsum  15415  lgseisenlem2  15766  gropd  15864  grstructd2dom  15865  ch2varv  16215  elab1  16230  elab2a  16231  elabg2  16232  cbvrald  16235  sumdc2  16246  bdsepnft  16333  bdsepnfALT  16335  bj-omssind  16381  bj-bdfindes  16395  bj-nn0suc0  16396  bj-nntrans  16397  bj-nnelirr  16399  bj-omtrans  16402  setindft  16411  bj-inf2vnlem3  16418  bj-inf2vnlem4  16419  bj-nn0sucALT  16424  bj-findis  16425  bj-findes  16427  strcollnft  16430  strcollnfALT  16432  pw1nct  16456  isomninnlem  16486  trilpolemeq1  16496  trirec0  16500  iswomninnlem  16505  ismkvnnlem  16508  nconstwlpolemgt0  16520