Theorem nfv 1577

Description: If 𝑥 is not present in 𝜑, then 𝑥 is not free in 𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.)

Assertion

Ref	Expression
nfv	⊢ Ⅎ𝑥𝜑

Distinct variable group:   𝜑,𝑥

Proof of Theorem nfv

Step	Hyp	Ref	Expression
1		ax-17 1575	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2	1	nfi 1511	1 ⊢ Ⅎ𝑥𝜑

Syntax hints:  Ⅎ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  2937  eqvincg  2944  eqvincf  2945  ceqsexgv  2949  elabgt  2961  elab  2964  elabg  2966  elab3g  2971  elrab3t  2975  elrab  2976  ralab2  2984  rexab2  2986  eqeu  2990  mosubt  2997  mo2icl  2999  mob2  3000  mob  3002  reu2  3008  reu3  3010  rmo4f  3018  nfcdeq  3042  sbcco  3067  sbcco2  3068  cbvsbcv  3075  sbcieg  3078  sbcie2g  3079  sbcied  3082  elrabsf  3084  sbcbidv  3104  sbcg  3115  sbc2iegf  3116  sbc2ie  3117  reu8nf  3127  rmo2ilem  3136  rmo3  3138  csbcow  3152  csbeq2dv  3167  nfcsb1d  3172  nfcsbd  3177  csbiebt  3181  csbied  3188  csbie2t  3190  sbcnestg  3195  sbnfc2  3202  cbvralcsf  3204  cbvrexcsf  3205  cbvreucsf  3206  cbvrabcsf  3207  cbvralv2  3208  cbvrexv2  3209  rspc2vd  3210  dfssf  3232  dfss2f  3233  uniiunlem  3332  abn0m  3538  rabn0m  3540  rabeq0  3542  abeq0  3543  r19.3rmv  3604  r19.28mv  3606  r19.27mv  3610  raaanv  3620  sbss  3621  nfifd  3654  rabsnifsb  3762  euabsn  3766  oprcl  3912  nfuni  3925  nfunid  3926  eluniab  3931  nfint  3964  elintab  3965  iineq2dv  4018  disjiun  4109  opabbidv  4181  nfopab  4183  cbvopab  4186  cbvopabv  4187  cbvopab1  4188  cbvopab2  4189  cbvopab1s  4190  cbvopab1v  4191  mpteq12f  4195  mpteq2dva  4205  cbvmptf  4209  cbvmpt  4210  zfrep6  4232  zfnuleu  4239  intexabim  4269  iinexgm  4271  repizf2  4280  bnd  4290  copsex2t  4366  copsex2g  4367  opelopabsb  4383  opelopabaf  4397  pofun  4438  frind  4478  reusv3  4586  alxfr  4587  rexxfrd  4589  ralxfrALT  4593  onintonm  4644  sucprcreg  4676  eunex  4688  tfis  4710  tfis2  4712  tfisi  4714  peano2  4722  findes  4730  omsinds  4749  opeliunxp  4810  opeliunxp2  4900  ralxpf  4906  rexxpf  4907  dfdmf  4954  reldmm  4980  dfrnf  5003  elrnmpt1  5013  intirr  5154  nfiotadw  5320  cbviota  5322  cbviotav  5324  sb8iota  5325  iota2d  5344  iota2  5347  dffun5r  5369  dffun6f  5370  dffun4f  5373  funco  5397  fun11  5428  imadif  5441  isarep1  5447  isarep2  5448  fun11iun  5640  fv3  5698  tz6.12f  5704  tz6.12c  5705  relelfvdm  5707  nfvres  5711  funimass4  5732  funfvdm2f  5747  fvmptss2  5757  fvmptdf  5770  fvmptdv  5771  fvmptt  5774  eqfnfv2f  5784  ralrnmpt  5824  rexrnmpt  5825  f1ompt  5833  ffnfv  5840  ffnfvf  5841  fmptco  5848  dfimafnf  5928  elabrex  5936  elabrexg  5937  dff13f  5949  fliftfun  5975  cbvriota  6023  cbvriotav  6024  riota2  6035  riotaeqimp  6036  riota5f  6038  acexmid  6057  nfoprab  6113  oprabbidv  6115  mpoeq123  6120  cbvoprab1  6133  cbvoprab2  6134  cbvoprab12  6135  cbvoprab12v  6136  cbvoprab3  6137  cbvoprab3v  6138  cbvmpox  6139  ralrnmpo  6176  ovmpodx  6188  ovmpodf  6193  ovmpodv  6194  ovi3  6199  ofrfval2  6292  abrexex2g  6322  opabex3d  6323  opabex3  6324  abrexex2  6326  elabreximdv  6330  uchoice  6344  dfoprab4f  6400  fmpox  6409  spc2ed  6442  cnvoprab  6443  f1od2  6444  opeliunxp2f  6482  tposoprab  6524  nfrecs  6551  tfri3  6611  nffrec  6640  eqerlem  6811  erovlem  6874  mptelixpg  6982  dom2lem  7024  modom  7074  xpf1o  7110  mapxpen  7114  nneneq  7124  findcard2  7159  findcard2s  7160  ac6sfi  7168  fiintim  7204  opabfi  7213  exmidomni  7446  fodjuomnilemdc  7448  ismkvnex  7459  mkvprop  7462  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  cc3  7598  indpi  7673  prarloclem3step  7827  prmuloc2  7898  ltexprlemm  7931  caucvgprprlemaddq  8039  caucvgsrlemgt1  8126  suplocsrlem  8139  axpre-suploclemres  8232  nn0ind-raph  9716  uzind4s  9943  indstr  9946  supinfneg  9948  infsupneg  9949  lbzbi  9969  fzrevral  10464  zsupcllemstep  10614  frecuzrdgtcl  10801  frecuzrdgfunlem  10808  nninfinf  10832  uzsinds  10833  seq3f1olemstep  10903  seq3f1olemp  10904  wrd2ind  11443  reuccatpfxs1  11467  fimaxre2  11940  climeu  12009  nfsum1  12069  nfsum  12070  sumrbdclem  12091  summodclem2a  12095  zsumdc  12098  fsum3  12101  isumss  12105  isumss2  12107  fsum3cvg2  12108  fsumsplitf  12122  fsum2dlemstep  12148  fsum00  12176  fsumrelem  12185  mertenslem2  12250  nfcprod1  12268  nfcprod  12269  prodeq2  12271  prodrbdclem  12285  prodmodclem2a  12290  zproddc  12293  fprodseq  12297  fprodntrivap  12298  prodssdc  12303  fprodcl2lem  12319  fprod2dlemstep  12336  fprodsplitf  12346  fprodsplit1f  12348  fprodap0f  12350  fprodle  12354  divalglemeunn  12635  divalglemeuneg  12637  bezoutlemnewy  12720  bezoutlemmain  12722  bezoutlemzz  12726  bezout  12735  nnwofdc  12762  prmind2  12845  oddpwdclemdvds  12895  oddpwdclemndvds  12896  pcmpt  13069  pcmptdvds  13071  exmidunben  13264  ctiunctlemfo  13277  ctiunct  13278  ctiunctal  13279  dfgrp3mlem  13856  gsumsplit0  14102  gfsumsn  14110  lss1d  14660  gsumfzfsumlemm  14864  cnmpt11  15277  cnmpt21  15285  cnmptcom  15292  imasnopn  15293  mulcncf  15602  ellimc3apf  15654  limccnp2cntop  15671  dvmptfsum  15719  lgseisenlem2  16073  gropd  16171  grstructd2dom  16172  ch2varv  16679  elab1  16694  elab2a  16695  elabg2  16696  cbvrald  16699  sumdc2  16710  bdsepnft  16796  bdsepnfALT  16798  bj-omssind  16844  bj-bdfindes  16858  bj-nn0suc0  16859  bj-nntrans  16860  bj-nnelirr  16862  bj-omtrans  16865  setindft  16874  bj-inf2vnlem3  16881  bj-inf2vnlem4  16882  bj-nn0sucALT  16887  bj-findis  16888  bj-findes  16890  strcollnft  16893  strcollnfALT  16895  pw1nct  16916  isomninnlem  16953  trilpolemeq1  16963  trirec0  16967  iswomninnlem  16973  ismkvnnlem  16976  nconstwlpolemgt0  16989