Theorem nfv 1581

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

This proof depends on syntax axioms:   F/wnf 1513

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1502  ax-17 1579

This proof depends on definitions:  df-bi 117  df-nf 1514

This theorem is used by:  nfvd  1582  alexim  1698  19.37aiv  1727  sbiedv  1842  spimv  1864  spimev  1914  19.36aiv  1957  cbval2  1977  cbvex2  1978  cbval2v  1979  cbvex2v  1980  cbvald  1981  cbvaldva  1984  cbvexdva  1985  eeanv  1992  nfsbv  2007  sbco2h  2024  nfsbt  2036  sbnf2  2041  dfsb7a  2054  sbalyz  2059  sbco4lem  2066  sbco4  2067  dvelimALT  2070  eubidv  2094  sb8eu  2099  nfeudv  2101  nfeud  2102  nfeuv  2104  nfeu  2105  mobidv  2122  mo23  2128  sbmo  2146  mo4  2148  moimv  2153  moanimv  2162  bm1.1  2223  eqsb1lem  2341  eqsb1  2342  clelsb1  2343  clelsb2  2344  abbibcom  2352  abbib  2356  abbidv  2358  cbvabv  2365  clelab  2366  nfcjust  2380  nfcv  2392  clelsb1f  2396  nfeqd  2407  nfeld  2408  nfabdw  2411  nfabd  2412  dvelimdc  2413  cleqf  2417  sbabel  2419  ralbidva  2546  rexbidva  2547  ralbidv  2550  rexbidv  2551  2ralbida  2571  2ralbidva  2572  nfraldya  2585  nfrexdya  2586  rgen2a  2604  ralimdva  2617  ralrimiv  2622  r19.21v  2627  ralrimdv  2629  reximdvai  2650  r19.23v  2660  rexlimiv  2662  rexlimdv  2667  r19.29af  2692  r19.29an  2693  r19.29a  2694  r19.32vr  2699  r19.37av  2704  r19.41v  2707  reean  2720  reeanv  2721  cbvrmow  2735  reubidva  2736  rmobidva  2741  cbvralf  2777  cbvrexf  2778  cbvreu  2784  cbvralv  2786  cbvrexv  2787  cbvreuv  2788  cbvrmov  2789  cbvralsv  2802  cbvrexsv  2803  sbralie  2804  cbvrab  2819  cbvrabv  2820  issetf  2829  ceqsalv  2852  ceqsralv  2853  ceqsexv  2861  ceqsex2  2863  ceqsex2v  2864  vtocld  2875  vtocl  2877  vtocl2  2878  vtocl3  2879  vtoclg  2883  vtocl2g  2887  vtoclga  2889  vtocl2gaf  2890  vtocl2ga  2891  vtocl3gaf  2892  vtocl3ga  2893  spcimdv  2909  spcimedv  2911  spcgv  2912  spcegv  2913  rspct  2922  rspc  2923  rspce  2924  rspcv  2925  rspcev  2929  rspc2v  2943  eqvincg  2950  eqvincf  2951  ceqsexgv  2955  elabgt  2967  elab  2970  elabg  2972  elab3g  2977  elrab3t  2981  elrab  2982  ralab2  2990  rexab2  2992  eqeu  2996  mosubt  3003  mo2icl  3005  mob2  3006  mob  3008  reu2  3014  reu3  3016  rmo4f  3024  nfcdeq  3048  sbcco  3073  sbcco2  3074  cbvsbcv  3081  sbcieg  3084  sbcie2g  3085  sbcied  3088  elrabsf  3090  sbcbidv  3110  sbcg  3121  sbc2iegf  3122  sbc2ie  3123  reu8nf  3133  rmo2ilem  3142  rmo3  3144  csbcow  3158  csbeq2dv  3173  nfcsb1d  3178  nfcsbd  3183  csbiebt  3187  csbied  3194  csbie2t  3196  sbcnestg  3201  sbnfc2  3208  cbvralcsf  3210  cbvrexcsf  3211  cbvreucsf  3212  cbvrabcsf  3213  cbvralv2  3214  cbvrexv2  3215  rspc2vd  3216  dfssf  3238  dfss2f  3239  uniiunlem  3338  abn0m  3547  rabn0m  3549  rabeq0  3552  abeq0  3553  r19.3rmv  3618  r19.28mv  3620  r19.27mv  3624  raaanv  3634  sbss  3635  nfifd  3668  rabsnifsb  3777  euabsn  3781  oprcl  3928  nfuni  3941  nfunid  3942  eluniab  3947  nfint  3980  elintab  3981  iineq2dv  4034  disjiun  4125  opabbidv  4197  nfopab  4199  cbvopab  4202  cbvopabv  4203  cbvopab1  4204  cbvopab2  4205  cbvopab1s  4206  cbvopab1v  4207  mpteq12f  4211  mpteq2dva  4221  cbvmptf  4225  cbvmpt  4226  zfrep6  4248  zfnuleu  4257  intexabim  4288  iinexgm  4290  repizf2  4299  bnd  4309  copsex2t  4385  copsex2g  4386  opelopabsb  4402  opelopabaf  4416  pofun  4457  frind  4497  reusv3  4606  alxfr  4607  rexxfrd  4609  ralxfrALT  4613  onintonm  4664  sucprcreg  4696  eunex  4708  tfis  4730  tfis2  4732  tfisi  4734  peano2  4742  findes  4750  omsinds  4769  opeliunxp  4830  opeliunxp2  4920  ralxpf  4926  rexxpf  4927  dfdmf  4974  reldmm  5000  dfrnf  5023  elrnmpt1  5033  intirr  5174  nfiotadw  5340  cbviota  5342  cbviotav  5344  sb8iota  5345  iota2d  5364  iota2  5367  dffun5r  5389  dffun6f  5390  dffun4f  5393  funco  5417  fun11  5448  imadif  5461  isarep1  5467  isarep2  5468  fun11iun  5660  fv3  5718  tz6.12f  5724  tz6.12c  5725  relelfvdm  5727  nfvres  5732  funimass4  5753  funfvdm2f  5768  fvmptss2  5780  fvmptdf  5793  fvmptdv  5794  fvmptt  5797  eqfnfv2f  5810  ralrnmpt  5850  rexrnmpt  5851  f1ompt  5859  ffnfv  5866  ffnfvf  5867  fmptco  5874  dfimafnf  5955  elabrex  5963  elabrexg  5964  dff13f  5976  fliftfun  6002  cbvriota  6050  cbvriotav  6051  riota2  6062  riotaeqimp  6063  riota5f  6065  acexmid  6084  nfoprab  6140  oprabbidv  6142  mpoeq123  6147  cbvoprab1  6160  cbvoprab2  6161  cbvoprab12  6162  cbvoprab12v  6163  cbvoprab3  6164  cbvoprab3v  6165  cbvmpox  6166  ralrnmpo  6203  ovmpodx  6215  ovmpodf  6220  ovmpodv  6221  ovi3  6226  ofrfval2  6319  abrexex2g  6349  opabex3d  6350  opabex3  6351  abrexex2  6353  elabreximdv  6357  uchoice  6371  dfoprab4f  6427  fmpox  6436  spc2ed  6469  cnvoprab  6470  f1od2  6471  opeliunxp2f  6509  tposoprab  6551  nfrecs  6578  tfri3  6638  nffrec  6667  eqerlem  6838  erovlem  6901  mptelixpg  7016  dom2lem  7058  modom  7108  xpf1o  7144  mapxpen  7148  nneneq  7158  findcard2  7193  findcard2s  7194  ac6sfi  7202  fiintim  7238  opabfi  7247  exmidomni  7483  fodjuomnilemdc  7485  ismkvnex  7496  mkvprop  7499  exmidfodomrlemr  7555  exmidfodomrlemrALT  7556  cc3  7635  indpi  7710  prarloclem3step  7864  prmuloc2  7935  ltexprlemm  7968  caucvgprprlemaddq  8076  caucvgsrlemgt1  8163  suplocsrlem  8176  axpre-suploclemres  8269  nn0ind-raph  9768  uzind4s  10000  indstr  10003  supinfneg  10005  infsupneg  10006  lbzbi  10026  fzrevral  10523  zsupcllemstep  10673  frecuzrdgtcl  10864  frecuzrdgfunlem  10871  nninfinf  10895  uzsinds  10896  seq3f1olemstep  10966  seq3f1olemp  10967  wrd2ind  11511  reuccatpfxs1  11535  fimaxre2  12010  climeu  12081  nfsum1  12141  nfsum  12142  sumrbdclem  12163  summodclem2a  12167  zsumdc  12170  fsum3  12173  isumss  12177  isumss2  12179  fsum3cvg2  12180  fsumsplitf  12194  fsum2dlemstep  12220  fsum00  12248  fsumrelem  12257  mertenslem2  12322  nfcprod1  12340  nfcprod  12341  prodeq2  12343  prodrbdclem  12357  prodmodclem2a  12362  zproddc  12365  fprodseq  12369  fprodntrivap  12370  prodssdc  12375  fprodcl2lem  12391  fprod2dlemstep  12408  fprodsplitf  12418  fprodsplit1f  12420  fprodap0f  12422  fprodle  12426  divalglemeunn  12707  divalglemeuneg  12709  bezoutlemnewy  12792  bezoutlemmain  12794  bezoutlemzz  12798  bezout  12807  nnwofdc  12834  prmind2  12917  nnmaxpwlemdvds  12968  nnmaxpwlemndvds  12969  pcmpt  13145  pcmptdvds  13147  exmidunben  13369  ctiunctlemfo  13382  ctiunct  13383  ctiunctal  13384  dfgrp3mlem  13956  gzsumsplit0  14232  gsumsncmn  14240  lss1d  14804  gsumfsum  15007  cnmpt11  15475  cnmpt21  15483  cnmptcom  15490  imasnopn  15491  mulcncf  15800  ellimc3apf  15852  limccnp2cntop  15869  dvmptfsum  15917  lgseisenlem2  16356  gropd  16454  grstructd2dom  16455  ch2varv  16962  elab1  16977  elab2a  16978  elabg2  16979  cbvrald  16982  sumdc2  16993  bdsepnft  17079  bdsepnfALT  17081  bj-omssind  17127  bj-bdfindes  17141  bj-nn0suc0  17142  bj-nntrans  17143  bj-nnelirr  17145  bj-omtrans  17148  setindft  17157  bj-inf2vnlem3  17164  bj-inf2vnlem4  17165  bj-nn0sucALT  17170  bj-findis  17171  bj-findes  17173  strcollnft  17176  strcollnfALT  17178  pw1nct  17199  isomninnlem  17245  trilpolemeq1  17256  trirec0  17260  iswomninnlem  17266  ismkvnnlem  17269  nconstwlpolemgt0  17281