Theorem nfv 1576

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 1574	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2	1	nfi 1510	1 ⊢ Ⅎ𝑥𝜑

Syntax hints:  Ⅎwnf 1508

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 1497  ax-17 1574

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

This theorem is referenced by:  nfvd  1577  alexim  1693  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  abbidv  2349  cbvabv  2356  clelab  2357  nfcjust  2362  nfcv  2374  clelsb1f  2378  nfeqd  2389  nfeld  2390  nfabdw  2393  nfabd  2394  dvelimdc  2395  cleqf  2399  sbabel  2401  ralbidva  2528  rexbidva  2529  ralbidv  2532  rexbidv  2533  2ralbida  2553  2ralbidva  2554  nfraldya  2567  nfrexdya  2568  rgen2a  2586  ralimdva  2599  ralrimiv  2604  r19.21v  2609  ralrimdv  2611  reximdvai  2632  r19.23v  2642  rexlimiv  2644  rexlimdv  2649  r19.29af  2674  r19.29an  2675  r19.29a  2676  r19.32vr  2681  r19.37av  2686  r19.41v  2689  reean  2702  reeanv  2703  cbvrmow  2716  reubidva  2717  rmobidva  2722  cbvralf  2758  cbvrexf  2759  cbvreu  2765  cbvralv  2767  cbvrexv  2768  cbvreuv  2769  cbvrmov  2770  cbvralsv  2783  cbvrexsv  2784  sbralie  2785  cbvrab  2800  cbvrabv  2801  issetf  2810  ceqsalv  2833  ceqsralv  2834  ceqsexv  2842  ceqsex2  2844  ceqsex2v  2845  vtocld  2856  vtocl  2858  vtocl2  2859  vtocl3  2860  vtoclg  2864  vtocl2g  2868  vtoclga  2870  vtocl2gaf  2871  vtocl2ga  2872  vtocl3gaf  2873  vtocl3ga  2874  spcimdv  2890  spcimedv  2892  spcgv  2893  spcegv  2894  rspct  2903  rspc  2904  rspce  2905  rspcv  2906  rspcev  2910  rspc2v  2923  eqvincg  2930  eqvincf  2931  ceqsexgv  2935  elabgt  2947  elab  2950  elabg  2952  elab3g  2957  elrab3t  2961  elrab  2962  ralab2  2970  rexab2  2972  eqeu  2976  mosubt  2983  mo2icl  2985  mob2  2986  mob  2988  reu2  2994  reu3  2996  rmo4f  3004  nfcdeq  3028  sbcco  3053  sbcco2  3054  cbvsbcv  3061  sbcieg  3064  sbcie2g  3065  sbcied  3068  elrabsf  3070  sbcbidv  3090  sbcg  3101  sbc2iegf  3102  sbc2ie  3103  reu8nf  3113  rmo2ilem  3122  rmo3  3124  csbcow  3138  csbeq2dv  3153  nfcsb1d  3158  nfcsbd  3163  csbiebt  3167  csbied  3174  csbie2t  3176  sbcnestg  3181  sbnfc2  3188  cbvralcsf  3190  cbvrexcsf  3191  cbvreucsf  3192  cbvrabcsf  3193  cbvralv2  3194  cbvrexv2  3195  rspc2vd  3196  dfss2f  3218  uniiunlem  3316  abn0m  3520  rabn0m  3522  rabeq0  3524  abeq0  3525  r19.3rmv  3585  r19.28mv  3587  r19.27mv  3591  raaanv  3601  sbss  3602  nfifd  3633  rabsnifsb  3737  euabsn  3741  oprcl  3886  nfuni  3899  nfunid  3900  eluniab  3905  nfint  3938  elintab  3939  iineq2dv  3992  disjiun  4083  opabbidv  4155  nfopab  4157  cbvopab  4160  cbvopabv  4161  cbvopab1  4162  cbvopab2  4163  cbvopab1s  4164  cbvopab1v  4165  mpteq12f  4169  mpteq2dva  4179  cbvmptf  4183  cbvmpt  4184  zfrep6  4206  zfnuleu  4213  intexabim  4242  iinexgm  4244  repizf2  4252  bnd  4262  copsex2t  4337  copsex2g  4338  opelopabsb  4354  opelopabaf  4368  pofun  4409  frind  4449  reusv3  4557  alxfr  4558  rexxfrd  4560  ralxfrALT  4564  onintonm  4615  sucprcreg  4647  eunex  4659  tfis  4681  tfis2  4683  tfisi  4685  peano2  4693  findes  4701  omsinds  4720  opeliunxp  4781  opeliunxp2  4870  ralxpf  4876  rexxpf  4877  dfdmf  4924  reldmm  4950  dfrnf  4973  elrnmpt1  4983  intirr  5123  nfiotadw  5289  cbviota  5291  cbviotav  5293  sb8iota  5294  iota2d  5313  iota2  5316  dffun5r  5338  dffun6f  5339  dffun4f  5342  funco  5366  fun11  5397  imadif  5410  isarep1  5416  isarep2  5417  fun11iun  5604  fv3  5662  tz6.12f  5668  tz6.12c  5669  relelfvdm  5671  nfvres  5675  funimass4  5696  funfvdm2f  5711  fvmptss2  5721  fvmptdf  5734  fvmptdv  5735  fvmptt  5738  eqfnfv2f  5748  ralrnmpt  5789  rexrnmpt  5790  f1ompt  5798  ffnfv  5805  ffnfvf  5806  fmptco  5813  elabrex  5898  elabrexg  5899  dff13f  5911  fliftfun  5937  cbvriota  5983  cbvriotav  5984  riota2  5995  riotaeqimp  5996  riota5f  5998  acexmid  6017  nfoprab  6073  oprabbidv  6075  mpoeq123  6080  cbvoprab1  6093  cbvoprab2  6094  cbvoprab12  6095  cbvoprab12v  6096  cbvoprab3  6097  cbvoprab3v  6098  cbvmpox  6099  ralrnmpo  6136  ovmpodx  6148  ovmpodf  6153  ovmpodv  6154  ovi3  6159  ofrfval2  6252  abrexex2g  6282  opabex3d  6283  opabex3  6284  abrexex2  6286  uchoice  6300  dfoprab4f  6356  fmpox  6365  spc2ed  6398  cnvoprab  6399  f1od2  6400  opeliunxp2f  6404  tposoprab  6446  nfrecs  6473  tfri3  6533  nffrec  6562  eqerlem  6733  erovlem  6796  mptelixpg  6903  dom2lem  6945  modom  6994  xpf1o  7030  mapxpen  7034  nneneq  7043  findcard2  7078  findcard2s  7079  ac6sfi  7087  fiintim  7123  opabfi  7132  exmidomni  7341  fodjuomnilemdc  7343  ismkvnex  7354  mkvprop  7357  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  cc3  7487  indpi  7562  prarloclem3step  7716  prmuloc2  7787  ltexprlemm  7820  caucvgprprlemaddq  7928  caucvgsrlemgt1  8015  suplocsrlem  8028  axpre-suploclemres  8121  nn0ind-raph  9597  uzind4s  9824  indstr  9827  supinfneg  9829  infsupneg  9830  lbzbi  9850  fzrevral  10340  zsupcllemstep  10490  frecuzrdgtcl  10675  frecuzrdgfunlem  10682  nninfinf  10706  uzsinds  10707  seq3f1olemstep  10777  seq3f1olemp  10778  wrd2ind  11308  reuccatpfxs1  11332  fimaxre2  11805  climeu  11874  nfsum1  11934  nfsum  11935  sumrbdclem  11956  summodclem2a  11960  zsumdc  11963  fsum3  11966  isumss  11970  isumss2  11972  fsum3cvg2  11973  fsumsplitf  11987  fsum2dlemstep  12013  fsum00  12041  fsumrelem  12050  mertenslem2  12115  nfcprod1  12133  nfcprod  12134  prodeq2  12136  prodrbdclem  12150  prodmodclem2a  12155  zproddc  12158  fprodseq  12162  fprodntrivap  12163  prodssdc  12168  fprodcl2lem  12184  fprod2dlemstep  12201  fprodsplitf  12211  fprodsplit1f  12213  fprodap0f  12215  fprodle  12219  divalglemeunn  12500  divalglemeuneg  12502  bezoutlemnewy  12585  bezoutlemmain  12587  bezoutlemzz  12591  bezout  12600  nnwofdc  12627  prmind2  12710  oddpwdclemdvds  12760  oddpwdclemndvds  12761  pcmpt  12934  pcmptdvds  12936  exmidunben  13065  ctiunctlemfo  13078  ctiunct  13079  ctiunctal  13080  dfgrp3mlem  13699  gsumsplit0  13951  lss1d  14416  gsumfzfsumlemm  14620  cnmpt11  15026  cnmpt21  15034  cnmptcom  15041  imasnopn  15042  mulcncf  15351  ellimc3apf  15403  limccnp2cntop  15420  dvmptfsum  15468  lgseisenlem2  15819  gropd  15917  grstructd2dom  15918  ch2varv  16415  elab1  16430  elab2a  16431  elabg2  16432  cbvrald  16435  sumdc2  16446  bdsepnft  16533  bdsepnfALT  16535  bj-omssind  16581  bj-bdfindes  16595  bj-nn0suc0  16596  bj-nntrans  16597  bj-nnelirr  16599  bj-omtrans  16602  setindft  16611  bj-inf2vnlem3  16618  bj-inf2vnlem4  16619  bj-nn0sucALT  16624  bj-findis  16625  bj-findes  16627  strcollnft  16630  strcollnfALT  16632  pw1nct  16655  isomninnlem  16685  trilpolemeq1  16695  trirec0  16699  iswomninnlem  16705  ismkvnnlem  16708  nconstwlpolemgt0  16720  gfsumsn  16737