Theorem nfv 1542

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

Syntax hints:  Ⅎwnf 1474

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 1463  ax-17 1540

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

This theorem is referenced by:  nfvd  1543  alexim  1659  19.37aiv  1689  sbiedv  1803  spimv  1825  spimev  1875  19.36aiv  1916  cbval2  1936  cbvex2  1937  cbval2v  1938  cbvex2v  1939  cbvald  1940  cbvaldva  1943  cbvexdva  1944  eeanv  1951  nfsbv  1966  sbco2h  1983  nfsbt  1995  sbnf2  2000  dfsb7a  2013  sbalyz  2018  sbco4lem  2025  sbco4  2026  dvelimALT  2029  eubidv  2053  sb8eu  2058  nfeudv  2060  nfeud  2061  nfeuv  2063  nfeu  2064  mobidv  2081  mo23  2086  sbmo  2104  mo4  2106  moimv  2111  moanimv  2120  bm1.1  2181  eqsb1lem  2299  eqsb1  2300  clelsb1  2301  clelsb2  2302  abbi  2310  abbidv  2314  cbvabv  2321  clelab  2322  nfcjust  2327  nfcv  2339  clelsb1f  2343  nfeqd  2354  nfeld  2355  nfabdw  2358  nfabd  2359  dvelimdc  2360  cleqf  2364  sbabel  2366  ralbidva  2493  rexbidva  2494  ralbidv  2497  rexbidv  2498  2ralbida  2518  2ralbidva  2519  nfraldya  2532  nfrexdya  2533  rgen2a  2551  ralimdva  2564  ralrimiv  2569  r19.21v  2574  ralrimdv  2576  reximdvai  2597  r19.23v  2606  rexlimiv  2608  rexlimdv  2613  r19.29af  2638  r19.29an  2639  r19.29a  2640  r19.32vr  2645  r19.37av  2650  r19.41v  2653  reean  2666  reeanv  2667  reubidva  2680  rmobidva  2685  cbvralf  2721  cbvrexf  2722  cbvreu  2727  cbvralv  2729  cbvrexv  2730  cbvreuv  2731  cbvrmov  2732  cbvralsv  2745  cbvrexsv  2746  sbralie  2747  cbvrab  2761  cbvrabv  2762  issetf  2770  ceqsalv  2793  ceqsralv  2794  ceqsexv  2802  ceqsex2  2804  ceqsex2v  2805  vtocld  2816  vtocl  2818  vtocl2  2819  vtocl3  2820  vtoclg  2824  vtocl2g  2828  vtoclga  2830  vtocl2gaf  2831  vtocl2ga  2832  vtocl3gaf  2833  vtocl3ga  2834  spcimdv  2848  spcimedv  2850  spcgv  2851  spcegv  2852  rspct  2861  rspc  2862  rspce  2863  rspcv  2864  rspcev  2868  rspc2v  2881  eqvincg  2888  eqvincf  2889  ceqsexgv  2893  elabgt  2905  elab  2908  elabg  2910  elab3g  2915  elrab3t  2919  elrab  2920  ralab2  2928  rexab2  2930  eqeu  2934  mosubt  2941  mo2icl  2943  mob2  2944  mob  2946  reu2  2952  reu3  2954  rmo4f  2962  nfcdeq  2986  sbcco  3011  sbcco2  3012  cbvsbcv  3019  sbcieg  3022  sbcie2g  3023  sbcied  3026  elrabsf  3028  sbcbidv  3048  sbcg  3059  sbc2iegf  3060  sbc2ie  3061  rmo2ilem  3079  rmo3  3081  csbcow  3095  csbeq2dv  3110  nfcsb1d  3115  nfcsbd  3120  csbiebt  3124  csbied  3131  csbie2t  3133  sbcnestg  3138  sbnfc2  3145  cbvralcsf  3147  cbvrexcsf  3148  cbvreucsf  3149  cbvrabcsf  3150  cbvralv2  3151  cbvrexv2  3152  rspc2vd  3153  dfss2f  3175  uniiunlem  3273  abn0m  3477  rabn0m  3479  rabeq0  3481  abeq0  3482  r19.3rmv  3542  r19.28mv  3544  r19.27mv  3548  raaanv  3558  sbss  3559  nfifd  3589  euabsn  3693  oprcl  3833  nfuni  3846  nfunid  3847  eluniab  3852  nfint  3885  elintab  3886  iineq2dv  3939  disjiun  4029  opabbidv  4100  nfopab  4102  cbvopab  4105  cbvopabv  4106  cbvopab1  4107  cbvopab2  4108  cbvopab1s  4109  cbvopab1v  4110  mpteq12f  4114  mpteq2dva  4124  cbvmptf  4128  cbvmpt  4129  zfrep6  4151  zfnuleu  4158  intexabim  4186  iinexgm  4188  repizf2  4196  bnd  4206  copsex2t  4279  copsex2g  4280  opelopabsb  4295  opelopabaf  4309  pofun  4348  frind  4388  reusv3  4496  alxfr  4497  rexxfrd  4499  ralxfrALT  4503  onintonm  4554  sucprcreg  4586  eunex  4598  tfis  4620  tfis2  4622  tfisi  4624  peano2  4632  findes  4640  omsinds  4659  opeliunxp  4719  opeliunxp2  4807  ralxpf  4813  rexxpf  4814  dfdmf  4860  dfrnf  4908  elrnmpt1  4918  intirr  5057  nfiotadw  5223  cbviota  5225  cbviotav  5226  sb8iota  5227  iota2d  5246  iota2  5249  dffun5r  5271  dffun6f  5272  dffun4f  5275  funco  5299  fun11  5326  imadif  5339  isarep1  5345  isarep2  5346  fun11iun  5528  fv3  5584  tz6.12f  5590  tz6.12c  5591  relelfvdm  5593  nfvres  5595  funimass4  5614  funfvdm2f  5629  fvmptss2  5639  fvmptdf  5652  fvmptdv  5653  fvmptt  5656  eqfnfv2f  5666  ralrnmpt  5707  rexrnmpt  5708  f1ompt  5716  ffnfv  5723  ffnfvf  5724  fmptco  5731  elabrex  5807  elabrexg  5808  dff13f  5820  fliftfun  5846  cbvriota  5891  cbvriotav  5892  riota2  5903  riota5f  5905  acexmid  5924  nfoprab  5978  oprabbidv  5980  mpoeq123  5985  cbvoprab1  5998  cbvoprab2  5999  cbvoprab12  6000  cbvoprab12v  6001  cbvoprab3  6002  cbvoprab3v  6003  cbvmpox  6004  ralrnmpo  6041  ovmpodx  6053  ovmpodf  6058  ovmpodv  6059  ovi3  6064  ofrfval2  6156  abrexex2g  6186  opabex3d  6187  opabex3  6188  abrexex2  6190  uchoice  6204  dfoprab4f  6260  fmpox  6267  spc2ed  6300  cnvoprab  6301  f1od2  6302  opeliunxp2f  6305  tposoprab  6347  nfrecs  6374  tfri3  6434  nffrec  6463  eqerlem  6632  erovlem  6695  mptelixpg  6802  dom2lem  6840  xpf1o  6914  mapxpen  6918  nneneq  6927  findcard2  6959  findcard2s  6960  ac6sfi  6968  fiintim  7001  opabfi  7008  exmidomni  7217  fodjuomnilemdc  7219  ismkvnex  7230  mkvprop  7233  exmidfodomrlemr  7283  exmidfodomrlemrALT  7284  cc3  7353  indpi  7428  prarloclem3step  7582  prmuloc2  7653  ltexprlemm  7686  caucvgprprlemaddq  7794  caucvgsrlemgt1  7881  suplocsrlem  7894  axpre-suploclemres  7987  nn0ind-raph  9462  uzind4s  9683  indstr  9686  supinfneg  9688  infsupneg  9689  lbzbi  9709  fzrevral  10199  zsupcllemstep  10338  frecuzrdgtcl  10523  frecuzrdgfunlem  10530  nninfinf  10554  uzsinds  10555  seq3f1olemstep  10625  seq3f1olemp  10626  fimaxre2  11411  climeu  11480  nfsum1  11540  nfsum  11541  sumrbdclem  11561  summodclem2a  11565  zsumdc  11568  fsum3  11571  isumss  11575  isumss2  11577  fsum3cvg2  11578  fsumsplitf  11592  fsum2dlemstep  11618  fsum00  11646  fsumrelem  11655  mertenslem2  11720  nfcprod1  11738  nfcprod  11739  prodeq2  11741  prodrbdclem  11755  prodmodclem2a  11760  zproddc  11763  fprodseq  11767  fprodntrivap  11768  prodssdc  11773  fprodcl2lem  11789  fprod2dlemstep  11806  fprodsplitf  11816  fprodsplit1f  11818  fprodap0f  11820  fprodle  11824  divalglemeunn  12105  divalglemeuneg  12107  bezoutlemnewy  12190  bezoutlemmain  12192  bezoutlemzz  12196  bezout  12205  nnwofdc  12232  prmind2  12315  oddpwdclemdvds  12365  oddpwdclemndvds  12366  pcmpt  12539  pcmptdvds  12541  exmidunben  12670  ctiunctlemfo  12683  ctiunct  12684  ctiunctal  12685  dfgrp3mlem  13302  lss1d  14017  gsumfzfsumlemm  14221  cnmpt11  14627  cnmpt21  14635  cnmptcom  14642  imasnopn  14643  mulcncf  14952  ellimc3apf  15004  limccnp2cntop  15021  dvmptfsum  15069  lgseisenlem2  15420  ch2varv  15522  elab1  15537  elab2a  15538  elabg2  15539  cbvrald  15542  sumdc2  15553  bdsepnft  15641  bdsepnfALT  15643  bj-omssind  15689  bj-bdfindes  15703  bj-nn0suc0  15704  bj-nntrans  15705  bj-nnelirr  15707  bj-omtrans  15710  setindft  15719  bj-inf2vnlem3  15726  bj-inf2vnlem4  15727  bj-nn0sucALT  15732  bj-findis  15733  bj-findes  15735  strcollnft  15738  strcollnfALT  15740  pw1nct  15758  isomninnlem  15787  trilpolemeq1  15797  trirec0  15801  iswomninnlem  15806  ismkvnnlem  15809  nconstwlpolemgt0  15821