Theorem nfv 1550

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

Syntax hints:  Ⅎwnf 1482

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 1471  ax-17 1548

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

This theorem is referenced by:  nfvd  1551  alexim  1667  19.37aiv  1697  sbiedv  1811  spimv  1833  spimev  1883  19.36aiv  1924  cbval2  1944  cbvex2  1945  cbval2v  1946  cbvex2v  1947  cbvald  1948  cbvaldva  1951  cbvexdva  1952  eeanv  1959  nfsbv  1974  sbco2h  1991  nfsbt  2003  sbnf2  2008  dfsb7a  2021  sbalyz  2026  sbco4lem  2033  sbco4  2034  dvelimALT  2037  eubidv  2061  sb8eu  2066  nfeudv  2068  nfeud  2069  nfeuv  2071  nfeu  2072  mobidv  2089  mo23  2094  sbmo  2112  mo4  2114  moimv  2119  moanimv  2128  bm1.1  2189  eqsb1lem  2307  eqsb1  2308  clelsb1  2309  clelsb2  2310  abbi  2318  abbidv  2322  cbvabv  2329  clelab  2330  nfcjust  2335  nfcv  2347  clelsb1f  2351  nfeqd  2362  nfeld  2363  nfabdw  2366  nfabd  2367  dvelimdc  2368  cleqf  2372  sbabel  2374  ralbidva  2501  rexbidva  2502  ralbidv  2505  rexbidv  2506  2ralbida  2526  2ralbidva  2527  nfraldya  2540  nfrexdya  2541  rgen2a  2559  ralimdva  2572  ralrimiv  2577  r19.21v  2582  ralrimdv  2584  reximdvai  2605  r19.23v  2614  rexlimiv  2616  rexlimdv  2621  r19.29af  2646  r19.29an  2647  r19.29a  2648  r19.32vr  2653  r19.37av  2658  r19.41v  2661  reean  2674  reeanv  2675  reubidva  2688  rmobidva  2693  cbvralf  2729  cbvrexf  2730  cbvreu  2735  cbvralv  2737  cbvrexv  2738  cbvreuv  2739  cbvrmov  2740  cbvralsv  2753  cbvrexsv  2754  sbralie  2755  cbvrab  2769  cbvrabv  2770  issetf  2778  ceqsalv  2801  ceqsralv  2802  ceqsexv  2810  ceqsex2  2812  ceqsex2v  2813  vtocld  2824  vtocl  2826  vtocl2  2827  vtocl3  2828  vtoclg  2832  vtocl2g  2836  vtoclga  2838  vtocl2gaf  2839  vtocl2ga  2840  vtocl3gaf  2841  vtocl3ga  2842  spcimdv  2856  spcimedv  2858  spcgv  2859  spcegv  2860  rspct  2869  rspc  2870  rspce  2871  rspcv  2872  rspcev  2876  rspc2v  2889  eqvincg  2896  eqvincf  2897  ceqsexgv  2901  elabgt  2913  elab  2916  elabg  2918  elab3g  2923  elrab3t  2927  elrab  2928  ralab2  2936  rexab2  2938  eqeu  2942  mosubt  2949  mo2icl  2951  mob2  2952  mob  2954  reu2  2960  reu3  2962  rmo4f  2970  nfcdeq  2994  sbcco  3019  sbcco2  3020  cbvsbcv  3027  sbcieg  3030  sbcie2g  3031  sbcied  3034  elrabsf  3036  sbcbidv  3056  sbcg  3067  sbc2iegf  3068  sbc2ie  3069  rmo2ilem  3087  rmo3  3089  csbcow  3103  csbeq2dv  3118  nfcsb1d  3123  nfcsbd  3128  csbiebt  3132  csbied  3139  csbie2t  3141  sbcnestg  3146  sbnfc2  3153  cbvralcsf  3155  cbvrexcsf  3156  cbvreucsf  3157  cbvrabcsf  3158  cbvralv2  3159  cbvrexv2  3160  rspc2vd  3161  dfss2f  3183  uniiunlem  3281  abn0m  3485  rabn0m  3487  rabeq0  3489  abeq0  3490  r19.3rmv  3550  r19.28mv  3552  r19.27mv  3556  raaanv  3566  sbss  3567  nfifd  3597  euabsn  3702  oprcl  3842  nfuni  3855  nfunid  3856  eluniab  3861  nfint  3894  elintab  3895  iineq2dv  3948  disjiun  4038  opabbidv  4109  nfopab  4111  cbvopab  4114  cbvopabv  4115  cbvopab1  4116  cbvopab2  4117  cbvopab1s  4118  cbvopab1v  4119  mpteq12f  4123  mpteq2dva  4133  cbvmptf  4137  cbvmpt  4138  zfrep6  4160  zfnuleu  4167  intexabim  4195  iinexgm  4197  repizf2  4205  bnd  4215  copsex2t  4288  copsex2g  4289  opelopabsb  4305  opelopabaf  4319  pofun  4358  frind  4398  reusv3  4506  alxfr  4507  rexxfrd  4509  ralxfrALT  4513  onintonm  4564  sucprcreg  4596  eunex  4608  tfis  4630  tfis2  4632  tfisi  4634  peano2  4642  findes  4650  omsinds  4669  opeliunxp  4729  opeliunxp2  4817  ralxpf  4823  rexxpf  4824  dfdmf  4870  dfrnf  4918  elrnmpt1  4928  intirr  5068  nfiotadw  5234  cbviota  5236  cbviotav  5237  sb8iota  5238  iota2d  5257  iota2  5260  dffun5r  5282  dffun6f  5283  dffun4f  5286  funco  5310  fun11  5340  imadif  5353  isarep1  5359  isarep2  5360  fun11iun  5542  fv3  5598  tz6.12f  5604  tz6.12c  5605  relelfvdm  5607  nfvres  5609  funimass4  5628  funfvdm2f  5643  fvmptss2  5653  fvmptdf  5666  fvmptdv  5667  fvmptt  5670  eqfnfv2f  5680  ralrnmpt  5721  rexrnmpt  5722  f1ompt  5730  ffnfv  5737  ffnfvf  5738  fmptco  5745  elabrex  5825  elabrexg  5826  dff13f  5838  fliftfun  5864  cbvriota  5909  cbvriotav  5910  riota2  5921  riota5f  5923  acexmid  5942  nfoprab  5996  oprabbidv  5998  mpoeq123  6003  cbvoprab1  6016  cbvoprab2  6017  cbvoprab12  6018  cbvoprab12v  6019  cbvoprab3  6020  cbvoprab3v  6021  cbvmpox  6022  ralrnmpo  6059  ovmpodx  6071  ovmpodf  6076  ovmpodv  6077  ovi3  6082  ofrfval2  6174  abrexex2g  6204  opabex3d  6205  opabex3  6206  abrexex2  6208  uchoice  6222  dfoprab4f  6278  fmpox  6285  spc2ed  6318  cnvoprab  6319  f1od2  6320  opeliunxp2f  6323  tposoprab  6365  nfrecs  6392  tfri3  6452  nffrec  6481  eqerlem  6650  erovlem  6713  mptelixpg  6820  dom2lem  6862  xpf1o  6940  mapxpen  6944  nneneq  6953  findcard2  6985  findcard2s  6986  ac6sfi  6994  fiintim  7027  opabfi  7034  exmidomni  7243  fodjuomnilemdc  7245  ismkvnex  7256  mkvprop  7259  exmidfodomrlemr  7309  exmidfodomrlemrALT  7310  cc3  7379  indpi  7454  prarloclem3step  7608  prmuloc2  7679  ltexprlemm  7712  caucvgprprlemaddq  7820  caucvgsrlemgt1  7907  suplocsrlem  7920  axpre-suploclemres  8013  nn0ind-raph  9489  uzind4s  9710  indstr  9713  supinfneg  9715  infsupneg  9716  lbzbi  9736  fzrevral  10226  zsupcllemstep  10370  frecuzrdgtcl  10555  frecuzrdgfunlem  10562  nninfinf  10586  uzsinds  10587  seq3f1olemstep  10657  seq3f1olemp  10658  fimaxre2  11509  climeu  11578  nfsum1  11638  nfsum  11639  sumrbdclem  11659  summodclem2a  11663  zsumdc  11666  fsum3  11669  isumss  11673  isumss2  11675  fsum3cvg2  11676  fsumsplitf  11690  fsum2dlemstep  11716  fsum00  11744  fsumrelem  11753  mertenslem2  11818  nfcprod1  11836  nfcprod  11837  prodeq2  11839  prodrbdclem  11853  prodmodclem2a  11858  zproddc  11861  fprodseq  11865  fprodntrivap  11866  prodssdc  11871  fprodcl2lem  11887  fprod2dlemstep  11904  fprodsplitf  11914  fprodsplit1f  11916  fprodap0f  11918  fprodle  11922  divalglemeunn  12203  divalglemeuneg  12205  bezoutlemnewy  12288  bezoutlemmain  12290  bezoutlemzz  12294  bezout  12303  nnwofdc  12330  prmind2  12413  oddpwdclemdvds  12463  oddpwdclemndvds  12464  pcmpt  12637  pcmptdvds  12639  exmidunben  12768  ctiunctlemfo  12781  ctiunct  12782  ctiunctal  12783  dfgrp3mlem  13401  lss1d  14116  gsumfzfsumlemm  14320  cnmpt11  14726  cnmpt21  14734  cnmptcom  14741  imasnopn  14742  mulcncf  15051  ellimc3apf  15103  limccnp2cntop  15120  dvmptfsum  15168  lgseisenlem2  15519  gropd  15615  grstructd2dom  15616  ch2varv  15666  elab1  15681  elab2a  15682  elabg2  15683  cbvrald  15686  sumdc2  15697  bdsepnft  15785  bdsepnfALT  15787  bj-omssind  15833  bj-bdfindes  15847  bj-nn0suc0  15848  bj-nntrans  15849  bj-nnelirr  15851  bj-omtrans  15854  setindft  15863  bj-inf2vnlem3  15870  bj-inf2vnlem4  15871  bj-nn0sucALT  15876  bj-findis  15877  bj-findes  15879  strcollnft  15882  strcollnfALT  15884  pw1nct  15902  isomninnlem  15931  trilpolemeq1  15941  trirec0  15945  iswomninnlem  15950  ismkvnnlem  15953  nconstwlpolemgt0  15965