Theorem nfv 1528

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

Syntax hints:   F/wnf 1460

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 1449  ax-17 1526

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

This theorem is referenced by:  nfvd  1529  alexim  1645  19.37aiv  1675  sbiedv  1789  spimv  1811  spimev  1861  19.36aiv  1901  cbval2  1921  cbvex2  1922  cbval2v  1923  cbvex2v  1924  cbvald  1925  cbvaldva  1928  cbvexdva  1929  eeanv  1932  nfsbv  1947  sbco2h  1964  nfsbt  1976  sbnf2  1981  dfsb7a  1994  sbalyz  1999  sbco4lem  2006  sbco4  2007  dvelimALT  2010  eubidv  2034  sb8eu  2039  nfeudv  2041  nfeud  2042  nfeuv  2044  nfeu  2045  mobidv  2062  mo23  2067  sbmo  2085  mo4  2087  moimv  2092  moanimv  2101  bm1.1  2162  eqsb1lem  2280  eqsb1  2281  clelsb1  2282  clelsb2  2283  abbi  2291  abbidv  2295  cbvabv  2302  clelab  2303  nfcjust  2307  nfcv  2319  clelsb1f  2323  nfeqd  2334  nfeld  2335  nfabdw  2338  nfabd  2339  dvelimdc  2340  cleqf  2344  sbabel  2346  ralbidva  2473  rexbidva  2474  ralbidv  2477  rexbidv  2478  2ralbida  2498  2ralbidva  2499  nfraldya  2512  nfrexdya  2513  rgen2a  2531  ralimdva  2544  ralrimiv  2549  r19.21v  2554  ralrimdv  2556  reximdvai  2577  r19.23v  2586  rexlimiv  2588  rexlimdv  2593  r19.29af  2618  r19.29an  2619  r19.29a  2620  r19.32vr  2625  r19.37av  2630  r19.41v  2633  reean  2646  reeanv  2647  reubidva  2660  rmobidva  2665  cbvralf  2697  cbvrexf  2698  cbvreu  2702  cbvralv  2704  cbvrexv  2705  cbvreuv  2706  cbvrmov  2707  cbvralsv  2720  cbvrexsv  2721  sbralie  2722  cbvrab  2736  cbvrabv  2737  issetf  2745  ceqsalv  2768  ceqsralv  2769  ceqsexv  2777  ceqsex2  2778  ceqsex2v  2779  vtocld  2790  vtocl  2792  vtocl2  2793  vtocl3  2794  vtoclg  2798  vtocl2g  2802  vtoclga  2804  vtocl2gaf  2805  vtocl2ga  2806  vtocl3gaf  2807  vtocl3ga  2808  spcimdv  2822  spcimedv  2824  spcgv  2825  spcegv  2826  rspct  2835  rspc  2836  rspce  2837  rspcv  2838  rspcev  2842  rspc2v  2855  eqvincg  2862  eqvincf  2863  ceqsexgv  2867  elabgt  2879  elab  2882  elabg  2884  elab3g  2889  elrab3t  2893  elrab  2894  ralab2  2902  rexab2  2904  eqeu  2908  mosubt  2915  mo2icl  2917  mob2  2918  mob  2920  reu2  2926  reu3  2928  rmo4f  2936  nfcdeq  2960  sbcco  2985  sbcco2  2986  cbvsbcv  2993  sbcieg  2996  sbcie2g  2997  sbcied  3000  elrabsf  3002  sbcbidv  3022  sbcg  3033  sbc2iegf  3034  sbc2ie  3035  rmo2ilem  3053  rmo3  3055  csbcow  3069  csbeq2dv  3084  nfcsb1d  3089  nfcsbd  3093  csbiebt  3097  csbied  3104  csbie2t  3106  sbcnestg  3111  sbnfc2  3118  cbvralcsf  3120  cbvrexcsf  3121  cbvreucsf  3122  cbvrabcsf  3123  cbvralv2  3124  cbvrexv2  3125  rspc2vd  3126  dfss2f  3147  uniiunlem  3245  abn0m  3449  rabn0m  3451  rabeq0  3453  abeq0  3454  r19.3rmv  3514  r19.28mv  3516  r19.27mv  3520  raaanv  3531  sbss  3532  nfifd  3562  euabsn  3663  oprcl  3803  nfuni  3816  nfunid  3817  eluniab  3822  nfint  3855  elintab  3856  iineq2dv  3909  disjiun  3999  opabbidv  4070  nfopab  4072  cbvopab  4075  cbvopabv  4076  cbvopab1  4077  cbvopab2  4078  cbvopab1s  4079  cbvopab1v  4080  mpteq12f  4084  mpteq2dva  4094  cbvmptf  4098  cbvmpt  4099  zfrep6  4121  zfnuleu  4128  intexabim  4153  iinexgm  4155  repizf2  4163  bnd  4173  copsex2t  4246  copsex2g  4247  opelopabsb  4261  opelopabaf  4274  pofun  4313  frind  4353  reusv3  4461  alxfr  4462  rexxfrd  4464  ralxfrALT  4468  onintonm  4517  sucprcreg  4549  eunex  4561  tfis  4583  tfis2  4585  tfisi  4587  peano2  4595  findes  4603  omsinds  4622  opeliunxp  4682  opeliunxp2  4768  ralxpf  4774  rexxpf  4775  dfdmf  4821  dfrnf  4869  elrnmpt1  4879  intirr  5016  nfiotadw  5182  cbviota  5184  cbviotav  5185  sb8iota  5186  iota2d  5204  iota2  5207  dffun5r  5229  dffun6f  5230  dffun4f  5233  funco  5257  fun11  5284  imadif  5297  isarep1  5303  isarep2  5304  fun11iun  5483  fv3  5539  tz6.12f  5545  tz6.12c  5546  relelfvdm  5548  nfvres  5549  funimass4  5567  funfvdm2f  5582  fvmptss2  5592  fvmptdf  5604  fvmptdv  5605  fvmptt  5608  eqfnfv2f  5618  ralrnmpt  5659  rexrnmpt  5660  f1ompt  5668  ffnfv  5675  ffnfvf  5676  fmptco  5683  elabrex  5759  dff13f  5771  fliftfun  5797  cbvriota  5841  cbvriotav  5842  riota2  5853  riota5f  5855  acexmid  5874  nfoprab  5927  oprabbidv  5929  mpoeq123  5934  cbvoprab1  5947  cbvoprab2  5948  cbvoprab12  5949  cbvoprab12v  5950  cbvoprab3  5951  cbvoprab3v  5952  cbvmpox  5953  ralrnmpo  5989  ovmpodx  6001  ovmpodf  6006  ovmpodv  6007  ovi3  6011  ofrfval2  6099  abrexex2g  6121  opabex3d  6122  opabex3  6123  abrexex2  6125  dfoprab4f  6194  fmpox  6201  spc2ed  6234  cnvoprab  6235  f1od2  6236  opeliunxp2f  6239  tposoprab  6281  nfrecs  6308  tfri3  6368  nffrec  6397  eqerlem  6566  erovlem  6627  mptelixpg  6734  dom2lem  6772  xpf1o  6844  mapxpen  6848  nneneq  6857  findcard2  6889  findcard2s  6890  ac6sfi  6898  fiintim  6928  exmidomni  7140  fodjuomnilemdc  7142  ismkvnex  7153  mkvprop  7156  exmidfodomrlemr  7201  exmidfodomrlemrALT  7202  cc3  7267  indpi  7341  prarloclem3step  7495  prmuloc2  7566  ltexprlemm  7599  caucvgprprlemaddq  7707  caucvgsrlemgt1  7794  suplocsrlem  7807  axpre-suploclemres  7900  nn0ind-raph  9370  uzind4s  9590  indstr  9593  supinfneg  9595  infsupneg  9596  lbzbi  9616  fzrevral  10105  frecuzrdgtcl  10412  frecuzrdgfunlem  10419  uzsinds  10442  seq3f1olemstep  10501  seq3f1olemp  10502  fimaxre2  11235  climeu  11304  nfsum1  11364  nfsum  11365  sumrbdclem  11385  summodclem2a  11389  zsumdc  11392  fsum3  11395  isumss  11399  isumss2  11401  fsum3cvg2  11402  fsumsplitf  11416  fsum2dlemstep  11442  fsum00  11470  fsumrelem  11479  mertenslem2  11544  nfcprod1  11562  nfcprod  11563  prodeq2  11565  prodrbdclem  11579  prodmodclem2a  11584  zproddc  11587  fprodseq  11591  fprodntrivap  11592  prodssdc  11597  fprodcl2lem  11613  fprod2dlemstep  11630  fprodsplitf  11640  fprodsplit1f  11642  fprodap0f  11644  fprodle  11648  divalglemeunn  11926  divalglemeuneg  11928  zsupcllemstep  11946  bezoutlemnewy  11997  bezoutlemmain  11999  bezoutlemzz  12003  bezout  12012  nnwofdc  12039  prmind2  12120  oddpwdclemdvds  12170  oddpwdclemndvds  12171  pcmpt  12341  pcmptdvds  12343  exmidunben  12427  ctiunctlemfo  12440  ctiunct  12441  ctiunctal  12442  dfgrp3mlem  12968  cnmpt11  13786  cnmpt21  13794  cnmptcom  13801  imasnopn  13802  mulcncf  14094  ellimc3apf  14132  limccnp2cntop  14149  lgseisenlem2  14454  ch2varv  14523  elab1  14538  elab2a  14539  elabg2  14540  cbvrald  14543  sumdc2  14554  bdsepnft  14642  bdsepnfALT  14644  bj-omssind  14690  bj-bdfindes  14704  bj-nn0suc0  14705  bj-nntrans  14706  bj-nnelirr  14708  bj-omtrans  14711  setindft  14720  bj-inf2vnlem3  14727  bj-inf2vnlem4  14728  bj-nn0sucALT  14733  bj-findis  14734  bj-findes  14736  strcollnft  14739  strcollnfALT  14741  pw1nct  14755  isomninnlem  14781  trilpolemeq1  14791  trirec0  14795  iswomninnlem  14800  ismkvnnlem  14803  nconstwlpolemgt0  14814