Theorem nfv 1521

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

Syntax hints:   F/wnf 1453

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1442  ax-17 1519

This theorem depends on definitions:  df-bi 116  df-nf 1454

This theorem is referenced by:  nfvd  1522  alexim  1638  19.37aiv  1668  sbiedv  1782  spimv  1804  spimev  1854  19.36aiv  1894  cbval2  1914  cbvex2  1915  cbval2v  1916  cbvex2v  1917  cbvald  1918  cbvaldva  1921  cbvexdva  1922  eeanv  1925  nfsbv  1940  sbco2h  1957  nfsbt  1969  sbnf2  1974  dfsb7a  1987  sbalyz  1992  sbco4lem  1999  sbco4  2000  dvelimALT  2003  eubidv  2027  sb8eu  2032  nfeudv  2034  nfeud  2035  nfeuv  2037  nfeu  2038  mobidv  2055  mo23  2060  sbmo  2078  mo4  2080  moimv  2085  moanimv  2094  bm1.1  2155  eqsb1lem  2273  eqsb1  2274  clelsb1  2275  clelsb2  2276  abbi  2284  abbidv  2288  cbvabv  2295  clelab  2296  nfcjust  2300  nfcv  2312  clelsb1f  2316  nfeqd  2327  nfeld  2328  nfabdw  2331  nfabd  2332  dvelimdc  2333  cleqf  2337  sbabel  2339  ralbidva  2466  rexbidva  2467  ralbidv  2470  rexbidv  2471  2ralbida  2491  2ralbidva  2492  nfraldya  2505  nfrexdya  2506  rgen2a  2524  ralimdva  2537  ralrimiv  2542  r19.21v  2547  ralrimdv  2549  reximdvai  2570  r19.23v  2579  rexlimiv  2581  rexlimdv  2586  r19.29af  2611  r19.29an  2612  r19.29a  2613  r19.32vr  2618  r19.37av  2623  r19.41v  2626  reean  2638  reeanv  2639  reubidva  2652  rmobidva  2657  cbvralf  2689  cbvrexf  2690  cbvreu  2694  cbvralv  2696  cbvrexv  2697  cbvreuv  2698  cbvrmov  2699  cbvralsv  2712  cbvrexsv  2713  sbralie  2714  cbvrab  2728  cbvrabv  2729  issetf  2737  ceqsalv  2760  ceqsralv  2761  ceqsexv  2769  ceqsex2  2770  ceqsex2v  2771  vtocld  2782  vtocl  2784  vtocl2  2785  vtocl3  2786  vtoclg  2790  vtocl2g  2794  vtoclga  2796  vtocl2gaf  2797  vtocl2ga  2798  vtocl3gaf  2799  vtocl3ga  2800  spcimdv  2814  spcimedv  2816  spcgv  2817  spcegv  2818  rspct  2827  rspc  2828  rspce  2829  rspcv  2830  rspcev  2834  rspc2v  2847  eqvincg  2854  eqvincf  2855  ceqsexgv  2859  elabgt  2871  elab  2874  elabg  2876  elab3g  2881  elrab3t  2885  elrab  2886  ralab2  2894  rexab2  2896  eqeu  2900  mosubt  2907  mo2icl  2909  mob2  2910  mob  2912  reu2  2918  reu3  2920  rmo4f  2928  nfcdeq  2952  sbcco  2976  sbcco2  2977  cbvsbcv  2984  sbcieg  2987  sbcie2g  2988  sbcied  2991  elrabsf  2993  sbcbidv  3013  sbcg  3024  sbc2iegf  3025  sbc2ie  3026  rmo2ilem  3044  rmo3  3046  csbcow  3060  csbeq2dv  3075  nfcsb1d  3080  nfcsbd  3084  csbiebt  3088  csbied  3095  csbie2t  3097  sbcnestg  3102  sbnfc2  3109  cbvralcsf  3111  cbvrexcsf  3112  cbvreucsf  3113  cbvrabcsf  3114  cbvralv2  3115  cbvrexv2  3116  rspc2vd  3117  dfss2f  3138  uniiunlem  3236  abn0m  3440  rabn0m  3442  rabeq0  3444  abeq0  3445  r19.3rmv  3505  r19.28mv  3507  r19.27mv  3511  raaanv  3522  sbss  3523  nfifd  3553  euabsn  3653  oprcl  3789  nfuni  3802  nfunid  3803  eluniab  3808  nfint  3841  elintab  3842  iineq2dv  3895  disjiun  3984  opabbidv  4055  nfopab  4057  cbvopab  4060  cbvopabv  4061  cbvopab1  4062  cbvopab2  4063  cbvopab1s  4064  cbvopab1v  4065  mpteq12f  4069  mpteq2dva  4079  cbvmptf  4083  cbvmpt  4084  zfrep6  4106  zfnuleu  4113  intexabim  4138  iinexgm  4140  repizf2  4148  bnd  4158  copsex2t  4230  copsex2g  4231  opelopabsb  4245  opelopabaf  4258  pofun  4297  frind  4337  reusv3  4445  alxfr  4446  rexxfrd  4448  ralxfrALT  4452  onintonm  4501  sucprcreg  4533  eunex  4545  tfis  4567  tfis2  4569  tfisi  4571  peano2  4579  findes  4587  omsinds  4606  opeliunxp  4666  opeliunxp2  4751  ralxpf  4757  rexxpf  4758  dfdmf  4804  dfrnf  4852  elrnmpt1  4862  intirr  4997  nfiotadw  5163  cbviota  5165  cbviotav  5166  sb8iota  5167  iota2d  5185  iota2  5188  dffun5r  5210  dffun6f  5211  dffun4f  5214  funco  5238  fun11  5265  imadif  5278  isarep1  5284  isarep2  5285  fun11iun  5463  fv3  5519  tz6.12f  5525  tz6.12c  5526  relelfvdm  5528  nfvres  5529  funimass4  5547  funfvdm2f  5561  fvmptss2  5571  fvmptdf  5583  fvmptdv  5584  fvmptt  5587  eqfnfv2f  5597  ralrnmpt  5638  rexrnmpt  5639  f1ompt  5647  ffnfv  5654  ffnfvf  5655  fmptco  5662  elabrex  5737  dff13f  5749  fliftfun  5775  cbvriota  5819  cbvriotav  5820  riota2  5831  riota5f  5833  acexmid  5852  nfoprab  5905  oprabbidv  5907  mpoeq123  5912  cbvoprab1  5925  cbvoprab2  5926  cbvoprab12  5927  cbvoprab12v  5928  cbvoprab3  5929  cbvoprab3v  5930  cbvmpox  5931  ralrnmpo  5967  ovmpodx  5979  ovmpodf  5984  ovmpodv  5985  ovi3  5989  ofrfval2  6077  abrexex2g  6099  opabex3d  6100  opabex3  6101  abrexex2  6103  dfoprab4f  6172  fmpox  6179  spc2ed  6212  cnvoprab  6213  f1od2  6214  opeliunxp2f  6217  tposoprab  6259  nfrecs  6286  tfri3  6346  nffrec  6375  eqerlem  6544  erovlem  6605  mptelixpg  6712  dom2lem  6750  xpf1o  6822  mapxpen  6826  nneneq  6835  findcard2  6867  findcard2s  6868  ac6sfi  6876  fiintim  6906  exmidomni  7118  fodjuomnilemdc  7120  ismkvnex  7131  mkvprop  7134  exmidfodomrlemr  7179  exmidfodomrlemrALT  7180  cc3  7230  indpi  7304  prarloclem3step  7458  prmuloc2  7529  ltexprlemm  7562  caucvgprprlemaddq  7670  caucvgsrlemgt1  7757  suplocsrlem  7770  axpre-suploclemres  7863  nn0ind-raph  9329  uzind4s  9549  indstr  9552  supinfneg  9554  infsupneg  9555  lbzbi  9575  fzrevral  10061  frecuzrdgtcl  10368  frecuzrdgfunlem  10375  uzsinds  10398  seq3f1olemstep  10457  seq3f1olemp  10458  fimaxre2  11190  climeu  11259  nfsum1  11319  nfsum  11320  sumrbdclem  11340  summodclem2a  11344  zsumdc  11347  fsum3  11350  isumss  11354  isumss2  11356  fsum3cvg2  11357  fsumsplitf  11371  fsum2dlemstep  11397  fsum00  11425  fsumrelem  11434  mertenslem2  11499  nfcprod1  11517  nfcprod  11518  prodeq2  11520  prodrbdclem  11534  prodmodclem2a  11539  zproddc  11542  fprodseq  11546  fprodntrivap  11547  prodssdc  11552  fprodcl2lem  11568  fprod2dlemstep  11585  fprodsplitf  11595  fprodsplit1f  11597  fprodap0f  11599  fprodle  11603  divalglemeunn  11880  divalglemeuneg  11882  zsupcllemstep  11900  bezoutlemnewy  11951  bezoutlemmain  11953  bezoutlemzz  11957  bezout  11966  nnwofdc  11993  prmind2  12074  oddpwdclemdvds  12124  oddpwdclemndvds  12125  pcmpt  12295  pcmptdvds  12297  exmidunben  12381  ctiunctlemfo  12394  ctiunct  12395  ctiunctal  12396  cnmpt11  13077  cnmpt21  13085  cnmptcom  13092  imasnopn  13093  mulcncf  13385  ellimc3apf  13423  limccnp2cntop  13440  ch2varv  13803  elab1  13818  elab2a  13819  elabg2  13820  cbvrald  13823  sumdc2  13834  bdsepnft  13922  bdsepnfALT  13924  bj-omssind  13970  bj-bdfindes  13984  bj-nn0suc0  13985  bj-nntrans  13986  bj-nnelirr  13988  bj-omtrans  13991  setindft  14000  bj-inf2vnlem3  14007  bj-inf2vnlem4  14008  bj-nn0sucALT  14013  bj-findis  14014  bj-findes  14016  strcollnft  14019  strcollnfALT  14021  pw1nct  14036  isomninnlem  14062  trilpolemeq1  14072  trirec0  14076  iswomninnlem  14081  ismkvnnlem  14084  nconstwlpolemgt0  14095