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  5897  elabrexg  5898  dff13f  5910  fliftfun  5936  cbvriota  5982  cbvriotav  5983  riota2  5994  riotaeqimp  5995  riota5f  5997  acexmid  6016  nfoprab  6072  oprabbidv  6074  mpoeq123  6079  cbvoprab1  6092  cbvoprab2  6093  cbvoprab12  6094  cbvoprab12v  6095  cbvoprab3  6096  cbvoprab3v  6097  cbvmpox  6098  ralrnmpo  6135  ovmpodx  6147  ovmpodf  6152  ovmpodv  6153  ovi3  6158  ofrfval2  6251  abrexex2g  6281  opabex3d  6282  opabex3  6283  abrexex2  6285  uchoice  6299  dfoprab4f  6355  fmpox  6364  spc2ed  6397  cnvoprab  6398  f1od2  6399  opeliunxp2f  6403  tposoprab  6445  nfrecs  6472  tfri3  6532  nffrec  6561  eqerlem  6732  erovlem  6795  mptelixpg  6902  dom2lem  6944  modom  6993  xpf1o  7029  mapxpen  7033  nneneq  7042  findcard2  7077  findcard2s  7078  ac6sfi  7086  fiintim  7122  opabfi  7131  exmidomni  7340  fodjuomnilemdc  7342  ismkvnex  7353  mkvprop  7356  exmidfodomrlemr  7412  exmidfodomrlemrALT  7413  cc3  7486  indpi  7561  prarloclem3step  7715  prmuloc2  7786  ltexprlemm  7819  caucvgprprlemaddq  7927  caucvgsrlemgt1  8014  suplocsrlem  8027  axpre-suploclemres  8120  nn0ind-raph  9596  uzind4s  9823  indstr  9826  supinfneg  9828  infsupneg  9829  lbzbi  9849  fzrevral  10339  zsupcllemstep  10488  frecuzrdgtcl  10673  frecuzrdgfunlem  10680  nninfinf  10704  uzsinds  10705  seq3f1olemstep  10775  seq3f1olemp  10776  wrd2ind  11303  reuccatpfxs1  11327  fimaxre2  11787  climeu  11856  nfsum1  11916  nfsum  11917  sumrbdclem  11937  summodclem2a  11941  zsumdc  11944  fsum3  11947  isumss  11951  isumss2  11953  fsum3cvg2  11954  fsumsplitf  11968  fsum2dlemstep  11994  fsum00  12022  fsumrelem  12031  mertenslem2  12096  nfcprod1  12114  nfcprod  12115  prodeq2  12117  prodrbdclem  12131  prodmodclem2a  12136  zproddc  12139  fprodseq  12143  fprodntrivap  12144  prodssdc  12149  fprodcl2lem  12165  fprod2dlemstep  12182  fprodsplitf  12192  fprodsplit1f  12194  fprodap0f  12196  fprodle  12200  divalglemeunn  12481  divalglemeuneg  12483  bezoutlemnewy  12566  bezoutlemmain  12568  bezoutlemzz  12572  bezout  12581  nnwofdc  12608  prmind2  12691  oddpwdclemdvds  12741  oddpwdclemndvds  12742  pcmpt  12915  pcmptdvds  12917  exmidunben  13046  ctiunctlemfo  13059  ctiunct  13060  ctiunctal  13061  dfgrp3mlem  13680  lss1d  14396  gsumfzfsumlemm  14600  cnmpt11  15006  cnmpt21  15014  cnmptcom  15021  imasnopn  15022  mulcncf  15331  ellimc3apf  15383  limccnp2cntop  15400  dvmptfsum  15448  lgseisenlem2  15799  gropd  15897  grstructd2dom  15898  ch2varv  16364  elab1  16379  elab2a  16380  elabg2  16381  cbvrald  16384  sumdc2  16395  bdsepnft  16482  bdsepnfALT  16484  bj-omssind  16530  bj-bdfindes  16544  bj-nn0suc0  16545  bj-nntrans  16546  bj-nnelirr  16548  bj-omtrans  16551  setindft  16560  bj-inf2vnlem3  16567  bj-inf2vnlem4  16568  bj-nn0sucALT  16573  bj-findis  16574  bj-findes  16576  strcollnft  16579  strcollnfALT  16581  pw1nct  16604  isomninnlem  16634  trilpolemeq1  16644  trirec0  16648  iswomninnlem  16653  ismkvnnlem  16656  nconstwlpolemgt0  16668