Theorem nfv 1577

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

Syntax hints:   F/wnf 1509

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 1498  ax-17 1575

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

This theorem is referenced by:  nfvd  1578  alexim  1694  19.37aiv  1723  sbiedv  1837  spimv  1859  spimev  1909  19.36aiv  1950  cbval2  1970  cbvex2  1971  cbval2v  1972  cbvex2v  1973  cbvald  1974  cbvaldva  1977  cbvexdva  1978  eeanv  1985  nfsbv  2000  sbco2h  2017  nfsbt  2029  sbnf2  2034  dfsb7a  2047  sbalyz  2052  sbco4lem  2059  sbco4  2060  dvelimALT  2063  eubidv  2087  sb8eu  2092  nfeudv  2094  nfeud  2095  nfeuv  2097  nfeu  2098  mobidv  2115  mo23  2121  sbmo  2139  mo4  2141  moimv  2146  moanimv  2155  bm1.1  2216  eqsb1lem  2334  eqsb1  2335  clelsb1  2336  clelsb2  2337  abbi  2345  abbib  2349  abbidv  2350  cbvabv  2357  clelab  2358  nfcjust  2363  nfcv  2375  clelsb1f  2379  nfeqd  2390  nfeld  2391  nfabdw  2394  nfabd  2395  dvelimdc  2396  cleqf  2400  sbabel  2402  ralbidva  2529  rexbidva  2530  ralbidv  2533  rexbidv  2534  2ralbida  2554  2ralbidva  2555  nfraldya  2568  nfrexdya  2569  rgen2a  2587  ralimdva  2600  ralrimiv  2605  r19.21v  2610  ralrimdv  2612  reximdvai  2633  r19.23v  2643  rexlimiv  2645  rexlimdv  2650  r19.29af  2675  r19.29an  2676  r19.29a  2677  r19.32vr  2682  r19.37av  2687  r19.41v  2690  reean  2703  reeanv  2704  cbvrmow  2717  reubidva  2718  rmobidva  2723  cbvralf  2759  cbvrexf  2760  cbvreu  2766  cbvralv  2768  cbvrexv  2769  cbvreuv  2770  cbvrmov  2771  cbvralsv  2784  cbvrexsv  2785  sbralie  2786  cbvrab  2801  cbvrabv  2802  issetf  2811  ceqsalv  2834  ceqsralv  2835  ceqsexv  2843  ceqsex2  2845  ceqsex2v  2846  vtocld  2857  vtocl  2859  vtocl2  2860  vtocl3  2861  vtoclg  2865  vtocl2g  2869  vtoclga  2871  vtocl2gaf  2872  vtocl2ga  2873  vtocl3gaf  2874  vtocl3ga  2875  spcimdv  2891  spcimedv  2893  spcgv  2894  spcegv  2895  rspct  2904  rspc  2905  rspce  2906  rspcv  2907  rspcev  2911  rspc2v  2924  eqvincg  2931  eqvincf  2932  ceqsexgv  2936  elabgt  2948  elab  2951  elabg  2953  elab3g  2958  elrab3t  2962  elrab  2963  ralab2  2971  rexab2  2973  eqeu  2977  mosubt  2984  mo2icl  2986  mob2  2987  mob  2989  reu2  2995  reu3  2997  rmo4f  3005  nfcdeq  3029  sbcco  3054  sbcco2  3055  cbvsbcv  3062  sbcieg  3065  sbcie2g  3066  sbcied  3069  elrabsf  3071  sbcbidv  3091  sbcg  3102  sbc2iegf  3103  sbc2ie  3104  reu8nf  3114  rmo2ilem  3123  rmo3  3125  csbcow  3139  csbeq2dv  3154  nfcsb1d  3159  nfcsbd  3164  csbiebt  3168  csbied  3175  csbie2t  3177  sbcnestg  3182  sbnfc2  3189  cbvralcsf  3191  cbvrexcsf  3192  cbvreucsf  3193  cbvrabcsf  3194  cbvralv2  3195  cbvrexv2  3196  rspc2vd  3197  dfss2f  3219  uniiunlem  3318  abn0m  3522  rabn0m  3524  rabeq0  3526  abeq0  3527  r19.3rmv  3587  r19.28mv  3589  r19.27mv  3593  raaanv  3603  sbss  3604  nfifd  3637  rabsnifsb  3741  euabsn  3745  oprcl  3891  nfuni  3904  nfunid  3905  eluniab  3910  nfint  3943  elintab  3944  iineq2dv  3997  disjiun  4088  opabbidv  4160  nfopab  4162  cbvopab  4165  cbvopabv  4166  cbvopab1  4167  cbvopab2  4168  cbvopab1s  4169  cbvopab1v  4170  mpteq12f  4174  mpteq2dva  4184  cbvmptf  4188  cbvmpt  4189  zfrep6  4211  zfnuleu  4218  intexabim  4247  iinexgm  4249  repizf2  4258  bnd  4268  copsex2t  4343  copsex2g  4344  opelopabsb  4360  opelopabaf  4374  pofun  4415  frind  4455  reusv3  4563  alxfr  4564  rexxfrd  4566  ralxfrALT  4570  onintonm  4621  sucprcreg  4653  eunex  4665  tfis  4687  tfis2  4689  tfisi  4691  peano2  4699  findes  4707  omsinds  4726  opeliunxp  4787  opeliunxp2  4876  ralxpf  4882  rexxpf  4883  dfdmf  4930  reldmm  4956  dfrnf  4979  elrnmpt1  4989  intirr  5130  nfiotadw  5296  cbviota  5298  cbviotav  5300  sb8iota  5301  iota2d  5320  iota2  5323  dffun5r  5345  dffun6f  5346  dffun4f  5349  funco  5373  fun11  5404  imadif  5417  isarep1  5423  isarep2  5424  fun11iun  5613  fv3  5671  tz6.12f  5677  tz6.12c  5678  relelfvdm  5680  nfvres  5684  funimass4  5705  funfvdm2f  5720  fvmptss2  5730  fvmptdf  5743  fvmptdv  5744  fvmptt  5747  eqfnfv2f  5757  ralrnmpt  5797  rexrnmpt  5798  f1ompt  5806  ffnfv  5813  ffnfvf  5814  fmptco  5821  elabrex  5908  elabrexg  5909  dff13f  5921  fliftfun  5947  cbvriota  5993  cbvriotav  5994  riota2  6005  riotaeqimp  6006  riota5f  6008  acexmid  6027  nfoprab  6083  oprabbidv  6085  mpoeq123  6090  cbvoprab1  6103  cbvoprab2  6104  cbvoprab12  6105  cbvoprab12v  6106  cbvoprab3  6107  cbvoprab3v  6108  cbvmpox  6109  ralrnmpo  6146  ovmpodx  6158  ovmpodf  6163  ovmpodv  6164  ovi3  6169  ofrfval2  6261  abrexex2g  6291  opabex3d  6292  opabex3  6293  abrexex2  6295  uchoice  6309  dfoprab4f  6365  fmpox  6374  spc2ed  6407  cnvoprab  6408  f1od2  6409  opeliunxp2f  6447  tposoprab  6489  nfrecs  6516  tfri3  6576  nffrec  6605  eqerlem  6776  erovlem  6839  mptelixpg  6946  dom2lem  6988  modom  7037  xpf1o  7073  mapxpen  7077  nneneq  7086  findcard2  7121  findcard2s  7122  ac6sfi  7130  fiintim  7166  opabfi  7175  exmidomni  7401  fodjuomnilemdc  7403  ismkvnex  7414  mkvprop  7417  exmidfodomrlemr  7473  exmidfodomrlemrALT  7474  cc3  7547  indpi  7622  prarloclem3step  7776  prmuloc2  7847  ltexprlemm  7880  caucvgprprlemaddq  7988  caucvgsrlemgt1  8075  suplocsrlem  8088  axpre-suploclemres  8181  nn0ind-raph  9658  uzind4s  9885  indstr  9888  supinfneg  9890  infsupneg  9891  lbzbi  9911  fzrevral  10402  zsupcllemstep  10552  frecuzrdgtcl  10737  frecuzrdgfunlem  10744  nninfinf  10768  uzsinds  10769  seq3f1olemstep  10839  seq3f1olemp  10840  wrd2ind  11370  reuccatpfxs1  11394  fimaxre2  11867  climeu  11936  nfsum1  11996  nfsum  11997  sumrbdclem  12018  summodclem2a  12022  zsumdc  12025  fsum3  12028  isumss  12032  isumss2  12034  fsum3cvg2  12035  fsumsplitf  12049  fsum2dlemstep  12075  fsum00  12103  fsumrelem  12112  mertenslem2  12177  nfcprod1  12195  nfcprod  12196  prodeq2  12198  prodrbdclem  12212  prodmodclem2a  12217  zproddc  12220  fprodseq  12224  fprodntrivap  12225  prodssdc  12230  fprodcl2lem  12246  fprod2dlemstep  12263  fprodsplitf  12273  fprodsplit1f  12275  fprodap0f  12277  fprodle  12281  divalglemeunn  12562  divalglemeuneg  12564  bezoutlemnewy  12647  bezoutlemmain  12649  bezoutlemzz  12653  bezout  12662  nnwofdc  12689  prmind2  12772  oddpwdclemdvds  12822  oddpwdclemndvds  12823  pcmpt  12996  pcmptdvds  12998  exmidunben  13127  ctiunctlemfo  13140  ctiunct  13141  ctiunctal  13142  dfgrp3mlem  13761  gsumsplit0  14013  lss1d  14479  gsumfzfsumlemm  14683  cnmpt11  15094  cnmpt21  15102  cnmptcom  15109  imasnopn  15110  mulcncf  15419  ellimc3apf  15471  limccnp2cntop  15488  dvmptfsum  15536  lgseisenlem2  15890  gropd  15988  grstructd2dom  15989  ch2varv  16486  elab1  16501  elab2a  16502  elabg2  16503  cbvrald  16506  sumdc2  16517  bdsepnft  16603  bdsepnfALT  16605  bj-omssind  16651  bj-bdfindes  16665  bj-nn0suc0  16666  bj-nntrans  16667  bj-nnelirr  16669  bj-omtrans  16672  setindft  16681  bj-inf2vnlem3  16688  bj-inf2vnlem4  16689  bj-nn0sucALT  16694  bj-findis  16695  bj-findes  16697  strcollnft  16700  strcollnfALT  16702  pw1nct  16725  isomninnlem  16762  trilpolemeq1  16772  trirec0  16776  iswomninnlem  16782  ismkvnnlem  16785  nconstwlpolemgt0  16797  gfsumsn  16814