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  7482  fodjuomnilemdc  7484  ismkvnex  7495  mkvprop  7498  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  cc3  7634  indpi  7709  prarloclem3step  7863  prmuloc2  7934  ltexprlemm  7967  caucvgprprlemaddq  8075  caucvgsrlemgt1  8162  suplocsrlem  8175  axpre-suploclemres  8268  nn0ind-raph  9763  uzind4s  9990  indstr  9993  supinfneg  9995  infsupneg  9996  lbzbi  10016  fzrevral  10512  zsupcllemstep  10662  frecuzrdgtcl  10849  frecuzrdgfunlem  10856  nninfinf  10880  uzsinds  10881  seq3f1olemstep  10951  seq3f1olemp  10952  wrd2ind  11495  reuccatpfxs1  11519  fimaxre2  11993  climeu  12062  nfsum1  12122  nfsum  12123  sumrbdclem  12144  summodclem2a  12148  zsumdc  12151  fsum3  12154  isumss  12158  isumss2  12160  fsum3cvg2  12161  fsumsplitf  12175  fsum2dlemstep  12201  fsum00  12229  fsumrelem  12238  mertenslem2  12303  nfcprod1  12321  nfcprod  12322  prodeq2  12324  prodrbdclem  12338  prodmodclem2a  12343  zproddc  12346  fprodseq  12350  fprodntrivap  12351  prodssdc  12356  fprodcl2lem  12372  fprod2dlemstep  12389  fprodsplitf  12399  fprodsplit1f  12401  fprodap0f  12403  fprodle  12407  divalglemeunn  12688  divalglemeuneg  12690  bezoutlemnewy  12773  bezoutlemmain  12775  bezoutlemzz  12779  bezout  12788  nnwofdc  12815  prmind2  12898  oddpwdclemdvds  12948  oddpwdclemndvds  12949  pcmpt  13122  pcmptdvds  13124  exmidunben  13317  ctiunctlemfo  13330  ctiunct  13331  ctiunctal  13332  dfgrp3mlem  13903  gzsumsplit0  14148  gsumsncmn  14156  lss1d  14720  gsumfsum  14923  cnmpt11  15384  cnmpt21  15392  cnmptcom  15399  imasnopn  15400  mulcncf  15709  ellimc3apf  15761  limccnp2cntop  15778  dvmptfsum  15826  lgseisenlem2  16190  gropd  16288  grstructd2dom  16289  ch2varv  16796  elab1  16811  elab2a  16812  elabg2  16813  cbvrald  16816  sumdc2  16827  bdsepnft  16913  bdsepnfALT  16915  bj-omssind  16961  bj-bdfindes  16975  bj-nn0suc0  16976  bj-nntrans  16977  bj-nnelirr  16979  bj-omtrans  16982  setindft  16991  bj-inf2vnlem3  16998  bj-inf2vnlem4  16999  bj-nn0sucALT  17004  bj-findis  17005  bj-findes  17007  strcollnft  17010  strcollnfALT  17012  pw1nct  17033  isomninnlem  17079  trilpolemeq1  17089  trirec0  17093  iswomninnlem  17099  ismkvnnlem  17102  nconstwlpolemgt0  17114