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  4198  nfopab  4200  cbvopab  4203  cbvopabv  4204  cbvopab1  4205  cbvopab2  4206  cbvopab1s  4207  cbvopab1v  4208  mpteq12f  4212  mpteq2dva  4223  cbvmptf  4227  cbvmpt  4228  zfrep6  4250  zfnuleu  4259  intexabim  4290  iinexgm  4292  repizf2  4301  bnd  4311  copsex2t  4387  copsex2g  4388  opelopabsb  4404  opelopabaf  4418  pofun  4459  frind  4499  reusv3  4608  alxfr  4609  rexxfrd  4611  ralxfrALT  4615  onintonm  4666  sucprcreg  4698  eunex  4710  tfis  4732  tfis2  4734  tfisi  4736  peano2  4744  findes  4752  omsinds  4771  opeliunxp  4832  opeliunxp2  4922  ralxpf  4928  rexxpf  4929  dfdmf  4976  reldmm  5002  dfrnf  5025  elrnmpt1  5035  intirr  5177  nfiotadw  5343  cbviota  5345  cbviotav  5347  sb8iota  5348  iota2d  5367  iota2  5370  dffun5r  5392  dffun6f  5393  dffun4f  5396  funco  5420  fun11  5451  imadif  5464  isarep1  5470  isarep2  5471  fun11iun  5663  fv3  5721  tz6.12f  5727  tz6.12c  5728  relelfvdm  5730  nfvres  5735  funimass4  5756  funfvdm2f  5771  fvmptss2  5783  fvmptdf  5796  fvmptdv  5797  fvmptt  5800  eqfnfv2f  5813  ralrnmpt  5853  rexrnmpt  5854  f1ompt  5862  ffnfv  5869  ffnfvf  5870  fmptco  5877  dfimafnf  5958  elabrex  5966  elabrexg  5967  dff13f  5979  fliftfun  6005  cbvriota  6053  cbvriotav  6054  riota2  6065  riotaeqimp  6066  riota5f  6068  acexmid  6087  nfoprab  6143  oprabbidv  6145  mpoeq123  6150  cbvoprab1  6163  cbvoprab2  6164  cbvoprab12  6165  cbvoprab12v  6166  cbvoprab3  6167  cbvoprab3v  6168  cbvmpox  6169  ralrnmpo  6206  ovmpodx  6218  ovmpodf  6223  ovmpodv  6224  ovi3  6229  ofrfval2  6323  abrexex2g  6353  opabex3d  6354  opabex3  6355  abrexex2  6357  elabreximdv  6361  uchoice  6375  dfoprab4f  6431  fmpox  6440  spc2ed  6473  cnvoprab  6474  f1od2  6475  opeliunxp2f  6513  tposoprab  6555  nfrecs  6582  tfri3  6642  nffrec  6671  eqerlem  6842  erovlem  6905  mptelixpg  7020  dom2lem  7062  modom  7112  xpf1o  7148  mapxpen  7152  nneneq  7162  findcard2  7197  findcard2s  7198  ac6sfi  7206  fiintim  7242  opabfi  7251  exmidomni  7488  fodjuomnilemdc  7490  ismkvnex  7501  mkvprop  7504  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  cc3  7640  indpi  7715  prarloclem3step  7869  prmuloc2  7940  ltexprlemm  7973  caucvgprprlemaddq  8081  caucvgsrlemgt1  8168  suplocsrlem  8181  axpre-suploclemres  8274  nn0ind-raph  9774  uzind4s  10006  indstr  10009  supinfneg  10011  infsupneg  10012  lbzbi  10032  fzrevral  10529  zsupcllemstep  10679  frecuzrdgtcl  10870  frecuzrdgfunlem  10877  nninfinf  10901  uzsinds  10902  seq3f1olemstep  10972  seq3f1olemp  10973  wrd2ind  11517  reuccatpfxs1  11541  fimaxre2  12016  climeu  12087  nfsum1  12147  nfsum  12148  sumrbdclem  12169  summodclem2a  12173  zsumdc  12176  fsum3  12179  isumss  12183  isumss2  12185  fsum3cvg2  12186  fsumsplitf  12200  fsum2dlemstep  12226  fsum00  12254  fsumrelem  12263  mertenslem2  12328  nfcprod1  12346  nfcprod  12347  prodeq2  12349  prodrbdclem  12363  prodmodclem2a  12368  zproddc  12371  fprodseq  12375  fprodntrivap  12376  prodssdc  12381  fprodcl2lem  12397  fprod2dlemstep  12414  fprodsplitf  12424  fprodsplit1f  12426  fprodap0f  12428  fprodle  12432  divalglemeunn  12713  divalglemeuneg  12715  bezoutlemnewy  12798  bezoutlemmain  12800  bezoutlemzz  12804  bezout  12813  nnwofdc  12840  prmind2  12923  nnmaxpwlemdvds  12974  nnmaxpwlemndvds  12975  pcmpt  13151  pcmptdvds  13153  exmidunben  13375  ctiunctlemfo  13388  ctiunct  13389  ctiunctal  13390  dfgrp3mlem  13962  gzsumsplit0  14238  gsumsncmn  14246  gsumsnfdcmn  14257  gsumsndcmn  14258  gsumunsnfd  14259  gsumcom2fi  14275  lss1d  14829  gsumfsum  15032  cnmpt11  15509  cnmpt21  15517  cnmptcom  15524  imasnopn  15525  mulcncf  15834  ellimc3apf  15886  limccnp2cntop  15903  dvmptfsum  15951  lgseisenlem2  16395  gropd  16493  grstructd2dom  16494  ch2varv  17001  elab1  17016  elab2a  17017  elabg2  17018  cbvrald  17021  sumdc2  17032  bdsepnft  17118  bdsepnfALT  17120  bj-omssind  17166  bj-bdfindes  17180  bj-nn0suc0  17181  bj-nntrans  17182  bj-nnelirr  17184  bj-omtrans  17187  setindft  17196  bj-inf2vnlem3  17203  bj-inf2vnlem4  17204  bj-nn0sucALT  17209  bj-findis  17210  bj-findes  17212  strcollnft  17215  strcollnfALT  17217  pw1nct  17238  isomninnlem  17285  trilpolemeq1  17296  trirec0  17300  iswomninnlem  17306  ismkvnnlem  17309  nconstwlpolemgt0  17321