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  1838  spimv  1860  spimev  1910  19.36aiv  1953  cbval2  1973  cbvex2  1974  cbval2v  1975  cbvex2v  1976  cbvald  1977  cbvaldva  1980  cbvexdva  1981  eeanv  1988  nfsbv  2003  sbco2h  2020  nfsbt  2032  sbnf2  2037  dfsb7a  2050  sbalyz  2055  sbco4lem  2062  sbco4  2063  dvelimALT  2066  eubidv  2090  sb8eu  2095  nfeudv  2097  nfeud  2098  nfeuv  2100  nfeu  2101  mobidv  2118  mo23  2124  sbmo  2142  mo4  2144  moimv  2149  moanimv  2158  bm1.1  2219  eqsb1lem  2337  eqsb1  2338  clelsb1  2339  clelsb2  2340  abbibcom  2348  abbib  2352  abbidv  2354  cbvabv  2361  clelab  2362  nfcjust  2374  nfcv  2386  clelsb1f  2390  nfeqd  2401  nfeld  2402  nfabdw  2405  nfabd  2406  dvelimdc  2407  cleqf  2411  sbabel  2413  ralbidva  2540  rexbidva  2541  ralbidv  2544  rexbidv  2545  2ralbida  2565  2ralbidva  2566  nfraldya  2579  nfrexdya  2580  rgen2a  2598  ralimdva  2611  ralrimiv  2616  r19.21v  2621  ralrimdv  2623  reximdvai  2644  r19.23v  2654  rexlimiv  2656  rexlimdv  2661  r19.29af  2686  r19.29an  2687  r19.29a  2688  r19.32vr  2693  r19.37av  2698  r19.41v  2701  reean  2714  reeanv  2715  cbvrmow  2729  reubidva  2730  rmobidva  2735  cbvralf  2771  cbvrexf  2772  cbvreu  2778  cbvralv  2780  cbvrexv  2781  cbvreuv  2782  cbvrmov  2783  cbvralsv  2796  cbvrexsv  2797  sbralie  2798  cbvrab  2813  cbvrabv  2814  issetf  2823  ceqsalv  2846  ceqsralv  2847  ceqsexv  2855  ceqsex2  2857  ceqsex2v  2858  vtocld  2869  vtocl  2871  vtocl2  2872  vtocl3  2873  vtoclg  2877  vtocl2g  2881  vtoclga  2883  vtocl2gaf  2884  vtocl2ga  2885  vtocl3gaf  2886  vtocl3ga  2887  spcimdv  2903  spcimedv  2905  spcgv  2906  spcegv  2907  rspct  2916  rspc  2917  rspce  2918  rspcv  2919  rspcev  2923  rspc2v  2936  eqvincg  2943  eqvincf  2944  ceqsexgv  2948  elabgt  2960  elab  2963  elabg  2965  elab3g  2970  elrab3t  2974  elrab  2975  ralab2  2983  rexab2  2985  eqeu  2989  mosubt  2996  mo2icl  2998  mob2  2999  mob  3001  reu2  3007  reu3  3009  rmo4f  3017  nfcdeq  3041  sbcco  3066  sbcco2  3067  cbvsbcv  3074  sbcieg  3077  sbcie2g  3078  sbcied  3081  elrabsf  3083  sbcbidv  3103  sbcg  3114  sbc2iegf  3115  sbc2ie  3116  reu8nf  3126  rmo2ilem  3135  rmo3  3137  csbcow  3151  csbeq2dv  3166  nfcsb1d  3171  nfcsbd  3176  csbiebt  3180  csbied  3187  csbie2t  3189  sbcnestg  3194  sbnfc2  3201  cbvralcsf  3203  cbvrexcsf  3204  cbvreucsf  3205  cbvrabcsf  3206  cbvralv2  3207  cbvrexv2  3208  rspc2vd  3209  dfss2f  3231  uniiunlem  3330  abn0m  3536  rabn0m  3538  rabeq0  3540  abeq0  3541  r19.3rmv  3602  r19.28mv  3604  r19.27mv  3608  raaanv  3618  sbss  3619  nfifd  3652  rabsnifsb  3759  euabsn  3763  oprcl  3909  nfuni  3922  nfunid  3923  eluniab  3928  nfint  3961  elintab  3962  iineq2dv  4015  disjiun  4106  opabbidv  4178  nfopab  4180  cbvopab  4183  cbvopabv  4184  cbvopab1  4185  cbvopab2  4186  cbvopab1s  4187  cbvopab1v  4188  mpteq12f  4192  mpteq2dva  4202  cbvmptf  4206  cbvmpt  4207  zfrep6  4229  zfnuleu  4236  intexabim  4266  iinexgm  4268  repizf2  4277  bnd  4287  copsex2t  4363  copsex2g  4364  opelopabsb  4380  opelopabaf  4394  pofun  4435  frind  4475  reusv3  4583  alxfr  4584  rexxfrd  4586  ralxfrALT  4590  onintonm  4641  sucprcreg  4673  eunex  4685  tfis  4707  tfis2  4709  tfisi  4711  peano2  4719  findes  4727  omsinds  4746  opeliunxp  4807  opeliunxp2  4897  ralxpf  4903  rexxpf  4904  dfdmf  4951  reldmm  4977  dfrnf  5000  elrnmpt1  5010  intirr  5151  nfiotadw  5317  cbviota  5319  cbviotav  5321  sb8iota  5322  iota2d  5341  iota2  5344  dffun5r  5366  dffun6f  5367  dffun4f  5370  funco  5394  fun11  5425  imadif  5438  isarep1  5444  isarep2  5445  fun11iun  5637  fv3  5695  tz6.12f  5701  tz6.12c  5702  relelfvdm  5704  nfvres  5708  funimass4  5729  funfvdm2f  5744  fvmptss2  5754  fvmptdf  5767  fvmptdv  5768  fvmptt  5771  eqfnfv2f  5781  ralrnmpt  5821  rexrnmpt  5822  f1ompt  5830  ffnfv  5837  ffnfvf  5838  fmptco  5845  elabrex  5932  elabrexg  5933  dff13f  5945  fliftfun  5971  cbvriota  6017  cbvriotav  6018  riota2  6029  riotaeqimp  6030  riota5f  6032  acexmid  6051  nfoprab  6107  oprabbidv  6109  mpoeq123  6114  cbvoprab1  6127  cbvoprab2  6128  cbvoprab12  6129  cbvoprab12v  6130  cbvoprab3  6131  cbvoprab3v  6132  cbvmpox  6133  ralrnmpo  6170  ovmpodx  6182  ovmpodf  6187  ovmpodv  6188  ovi3  6193  ofrfval2  6285  abrexex2g  6315  opabex3d  6316  opabex3  6317  abrexex2  6319  uchoice  6333  dfoprab4f  6389  fmpox  6398  spc2ed  6431  cnvoprab  6432  f1od2  6433  opeliunxp2f  6471  tposoprab  6513  nfrecs  6540  tfri3  6600  nffrec  6629  eqerlem  6800  erovlem  6863  mptelixpg  6971  dom2lem  7013  modom  7063  xpf1o  7099  mapxpen  7103  nneneq  7113  findcard2  7148  findcard2s  7149  ac6sfi  7157  fiintim  7193  opabfi  7202  exmidomni  7435  fodjuomnilemdc  7437  ismkvnex  7448  mkvprop  7451  exmidfodomrlemr  7507  exmidfodomrlemrALT  7508  cc3  7584  indpi  7659  prarloclem3step  7813  prmuloc2  7884  ltexprlemm  7917  caucvgprprlemaddq  8025  caucvgsrlemgt1  8112  suplocsrlem  8125  axpre-suploclemres  8218  nn0ind-raph  9698  uzind4s  9925  indstr  9928  supinfneg  9930  infsupneg  9931  lbzbi  9951  fzrevral  10443  zsupcllemstep  10593  frecuzrdgtcl  10778  frecuzrdgfunlem  10785  nninfinf  10809  uzsinds  10810  seq3f1olemstep  10880  seq3f1olemp  10881  wrd2ind  11419  reuccatpfxs1  11443  fimaxre2  11916  climeu  11985  nfsum1  12045  nfsum  12046  sumrbdclem  12067  summodclem2a  12071  zsumdc  12074  fsum3  12077  isumss  12081  isumss2  12083  fsum3cvg2  12084  fsumsplitf  12098  fsum2dlemstep  12124  fsum00  12152  fsumrelem  12161  mertenslem2  12226  nfcprod1  12244  nfcprod  12245  prodeq2  12247  prodrbdclem  12261  prodmodclem2a  12266  zproddc  12269  fprodseq  12273  fprodntrivap  12274  prodssdc  12279  fprodcl2lem  12295  fprod2dlemstep  12312  fprodsplitf  12322  fprodsplit1f  12324  fprodap0f  12326  fprodle  12330  divalglemeunn  12611  divalglemeuneg  12613  bezoutlemnewy  12696  bezoutlemmain  12698  bezoutlemzz  12702  bezout  12711  nnwofdc  12738  prmind2  12821  oddpwdclemdvds  12871  oddpwdclemndvds  12872  pcmpt  13045  pcmptdvds  13047  exmidunben  13194  ctiunctlemfo  13207  ctiunct  13208  ctiunctal  13209  dfgrp3mlem  13828  gsumsplit0  14080  lss1d  14548  gsumfzfsumlemm  14752  cnmpt11  15165  cnmpt21  15173  cnmptcom  15180  imasnopn  15181  mulcncf  15490  ellimc3apf  15542  limccnp2cntop  15559  dvmptfsum  15607  lgseisenlem2  15961  gropd  16059  grstructd2dom  16060  ch2varv  16557  elab1  16572  elab2a  16573  elabg2  16574  cbvrald  16577  sumdc2  16588  bdsepnft  16674  bdsepnfALT  16676  bj-omssind  16722  bj-bdfindes  16736  bj-nn0suc0  16737  bj-nntrans  16738  bj-nnelirr  16740  bj-omtrans  16743  setindft  16752  bj-inf2vnlem3  16759  bj-inf2vnlem4  16760  bj-nn0sucALT  16765  bj-findis  16766  bj-findes  16768  strcollnft  16771  strcollnfALT  16773  pw1nct  16794  isomninnlem  16831  trilpolemeq1  16841  trirec0  16845  iswomninnlem  16851  ismkvnnlem  16854  nconstwlpolemgt0  16867  gfsumsn  16884