Theorem nfv 1574

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

Syntax hints:  Ⅎwnf 1506

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 1495  ax-17 1572

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

This theorem is referenced by:  nfvd  1575  alexim  1691  19.37aiv  1721  sbiedv  1835  spimv  1857  spimev  1907  19.36aiv  1948  cbval2  1968  cbvex2  1969  cbval2v  1970  cbvex2v  1971  cbvald  1972  cbvaldva  1975  cbvexdva  1976  eeanv  1983  nfsbv  1998  sbco2h  2015  nfsbt  2027  sbnf2  2032  dfsb7a  2045  sbalyz  2050  sbco4lem  2057  sbco4  2058  dvelimALT  2061  eubidv  2085  sb8eu  2090  nfeudv  2092  nfeud  2093  nfeuv  2095  nfeu  2096  mobidv  2113  mo23  2119  sbmo  2137  mo4  2139  moimv  2144  moanimv  2153  bm1.1  2214  eqsb1lem  2332  eqsb1  2333  clelsb1  2334  clelsb2  2335  abbi  2343  abbidv  2347  cbvabv  2354  clelab  2355  nfcjust  2360  nfcv  2372  clelsb1f  2376  nfeqd  2387  nfeld  2388  nfabdw  2391  nfabd  2392  dvelimdc  2393  cleqf  2397  sbabel  2399  ralbidva  2526  rexbidva  2527  ralbidv  2530  rexbidv  2531  2ralbida  2551  2ralbidva  2552  nfraldya  2565  nfrexdya  2566  rgen2a  2584  ralimdva  2597  ralrimiv  2602  r19.21v  2607  ralrimdv  2609  reximdvai  2630  r19.23v  2640  rexlimiv  2642  rexlimdv  2647  r19.29af  2672  r19.29an  2673  r19.29a  2674  r19.32vr  2679  r19.37av  2684  r19.41v  2687  reean  2700  reeanv  2701  cbvrmow  2714  reubidva  2715  rmobidva  2720  cbvralf  2756  cbvrexf  2757  cbvreu  2763  cbvralv  2765  cbvrexv  2766  cbvreuv  2767  cbvrmov  2768  cbvralsv  2781  cbvrexsv  2782  sbralie  2783  cbvrab  2798  cbvrabv  2799  issetf  2808  ceqsalv  2831  ceqsralv  2832  ceqsexv  2840  ceqsex2  2842  ceqsex2v  2843  vtocld  2854  vtocl  2856  vtocl2  2857  vtocl3  2858  vtoclg  2862  vtocl2g  2866  vtoclga  2868  vtocl2gaf  2869  vtocl2ga  2870  vtocl3gaf  2871  vtocl3ga  2872  spcimdv  2888  spcimedv  2890  spcgv  2891  spcegv  2892  rspct  2901  rspc  2902  rspce  2903  rspcv  2904  rspcev  2908  rspc2v  2921  eqvincg  2928  eqvincf  2929  ceqsexgv  2933  elabgt  2945  elab  2948  elabg  2950  elab3g  2955  elrab3t  2959  elrab  2960  ralab2  2968  rexab2  2970  eqeu  2974  mosubt  2981  mo2icl  2983  mob2  2984  mob  2986  reu2  2992  reu3  2994  rmo4f  3002  nfcdeq  3026  sbcco  3051  sbcco2  3052  cbvsbcv  3059  sbcieg  3062  sbcie2g  3063  sbcied  3066  elrabsf  3068  sbcbidv  3088  sbcg  3099  sbc2iegf  3100  sbc2ie  3101  reu8nf  3111  rmo2ilem  3120  rmo3  3122  csbcow  3136  csbeq2dv  3151  nfcsb1d  3156  nfcsbd  3161  csbiebt  3165  csbied  3172  csbie2t  3174  sbcnestg  3179  sbnfc2  3186  cbvralcsf  3188  cbvrexcsf  3189  cbvreucsf  3190  cbvrabcsf  3191  cbvralv2  3192  cbvrexv2  3193  rspc2vd  3194  dfss2f  3216  uniiunlem  3314  abn0m  3518  rabn0m  3520  rabeq0  3522  abeq0  3523  r19.3rmv  3583  r19.28mv  3585  r19.27mv  3589  raaanv  3599  sbss  3600  nfifd  3631  rabsnifsb  3735  euabsn  3739  oprcl  3884  nfuni  3897  nfunid  3898  eluniab  3903  nfint  3936  elintab  3937  iineq2dv  3990  disjiun  4081  opabbidv  4153  nfopab  4155  cbvopab  4158  cbvopabv  4159  cbvopab1  4160  cbvopab2  4161  cbvopab1s  4162  cbvopab1v  4163  mpteq12f  4167  mpteq2dva  4177  cbvmptf  4181  cbvmpt  4182  zfrep6  4204  zfnuleu  4211  intexabim  4240  iinexgm  4242  repizf2  4250  bnd  4260  copsex2t  4335  copsex2g  4336  opelopabsb  4352  opelopabaf  4366  pofun  4407  frind  4447  reusv3  4555  alxfr  4556  rexxfrd  4558  ralxfrALT  4562  onintonm  4613  sucprcreg  4645  eunex  4657  tfis  4679  tfis2  4681  tfisi  4683  peano2  4691  findes  4699  omsinds  4718  opeliunxp  4779  opeliunxp2  4868  ralxpf  4874  rexxpf  4875  dfdmf  4922  reldmm  4948  dfrnf  4971  elrnmpt1  4981  intirr  5121  nfiotadw  5287  cbviota  5289  cbviotav  5291  sb8iota  5292  iota2d  5311  iota2  5314  dffun5r  5336  dffun6f  5337  dffun4f  5340  funco  5364  fun11  5394  imadif  5407  isarep1  5413  isarep2  5414  fun11iun  5601  fv3  5658  tz6.12f  5664  tz6.12c  5665  relelfvdm  5667  nfvres  5671  funimass4  5692  funfvdm2f  5707  fvmptss2  5717  fvmptdf  5730  fvmptdv  5731  fvmptt  5734  eqfnfv2f  5744  ralrnmpt  5785  rexrnmpt  5786  f1ompt  5794  ffnfv  5801  ffnfvf  5802  fmptco  5809  elabrex  5893  elabrexg  5894  dff13f  5906  fliftfun  5932  cbvriota  5978  cbvriotav  5979  riota2  5990  riotaeqimp  5991  riota5f  5993  acexmid  6012  nfoprab  6068  oprabbidv  6070  mpoeq123  6075  cbvoprab1  6088  cbvoprab2  6089  cbvoprab12  6090  cbvoprab12v  6091  cbvoprab3  6092  cbvoprab3v  6093  cbvmpox  6094  ralrnmpo  6131  ovmpodx  6143  ovmpodf  6148  ovmpodv  6149  ovi3  6154  ofrfval2  6247  abrexex2g  6277  opabex3d  6278  opabex3  6279  abrexex2  6281  uchoice  6295  dfoprab4f  6351  fmpox  6360  spc2ed  6393  cnvoprab  6394  f1od2  6395  opeliunxp2f  6399  tposoprab  6441  nfrecs  6468  tfri3  6528  nffrec  6557  eqerlem  6728  erovlem  6791  mptelixpg  6898  dom2lem  6940  modom  6989  xpf1o  7025  mapxpen  7029  nneneq  7038  findcard2  7071  findcard2s  7072  ac6sfi  7080  fiintim  7116  opabfi  7123  exmidomni  7332  fodjuomnilemdc  7334  ismkvnex  7345  mkvprop  7348  exmidfodomrlemr  7403  exmidfodomrlemrALT  7404  cc3  7477  indpi  7552  prarloclem3step  7706  prmuloc2  7777  ltexprlemm  7810  caucvgprprlemaddq  7918  caucvgsrlemgt1  8005  suplocsrlem  8018  axpre-suploclemres  8111  nn0ind-raph  9587  uzind4s  9814  indstr  9817  supinfneg  9819  infsupneg  9820  lbzbi  9840  fzrevral  10330  zsupcllemstep  10479  frecuzrdgtcl  10664  frecuzrdgfunlem  10671  nninfinf  10695  uzsinds  10696  seq3f1olemstep  10766  seq3f1olemp  10767  wrd2ind  11294  reuccatpfxs1  11318  fimaxre2  11778  climeu  11847  nfsum1  11907  nfsum  11908  sumrbdclem  11928  summodclem2a  11932  zsumdc  11935  fsum3  11938  isumss  11942  isumss2  11944  fsum3cvg2  11945  fsumsplitf  11959  fsum2dlemstep  11985  fsum00  12013  fsumrelem  12022  mertenslem2  12087  nfcprod1  12105  nfcprod  12106  prodeq2  12108  prodrbdclem  12122  prodmodclem2a  12127  zproddc  12130  fprodseq  12134  fprodntrivap  12135  prodssdc  12140  fprodcl2lem  12156  fprod2dlemstep  12173  fprodsplitf  12183  fprodsplit1f  12185  fprodap0f  12187  fprodle  12191  divalglemeunn  12472  divalglemeuneg  12474  bezoutlemnewy  12557  bezoutlemmain  12559  bezoutlemzz  12563  bezout  12572  nnwofdc  12599  prmind2  12682  oddpwdclemdvds  12732  oddpwdclemndvds  12733  pcmpt  12906  pcmptdvds  12908  exmidunben  13037  ctiunctlemfo  13050  ctiunct  13051  ctiunctal  13052  dfgrp3mlem  13671  lss1d  14387  gsumfzfsumlemm  14591  cnmpt11  14997  cnmpt21  15005  cnmptcom  15012  imasnopn  15013  mulcncf  15322  ellimc3apf  15374  limccnp2cntop  15391  dvmptfsum  15439  lgseisenlem2  15790  gropd  15888  grstructd2dom  15889  ch2varv  16300  elab1  16315  elab2a  16316  elabg2  16317  cbvrald  16320  sumdc2  16331  bdsepnft  16418  bdsepnfALT  16420  bj-omssind  16466  bj-bdfindes  16480  bj-nn0suc0  16481  bj-nntrans  16482  bj-nnelirr  16484  bj-omtrans  16487  setindft  16496  bj-inf2vnlem3  16503  bj-inf2vnlem4  16504  bj-nn0sucALT  16509  bj-findis  16510  bj-findes  16512  strcollnft  16515  strcollnfALT  16517  pw1nct  16540  isomninnlem  16570  trilpolemeq1  16580  trirec0  16584  iswomninnlem  16589  ismkvnnlem  16592  nconstwlpolemgt0  16604