Theorem nfv 1577

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

Syntax hints:  Ⅎwnf 1509

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 1498  ax-17 1575

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

This theorem is referenced by:  nfvd  1578  alexim  1694  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  abbib  2349  abbidv  2350  cbvabv  2357  clelab  2358  nfcjust  2363  nfcv  2375  clelsb1f  2379  nfeqd  2390  nfeld  2391  nfabdw  2394  nfabd  2395  dvelimdc  2396  cleqf  2400  sbabel  2402  ralbidva  2529  rexbidva  2530  ralbidv  2533  rexbidv  2534  2ralbida  2554  2ralbidva  2555  nfraldya  2568  nfrexdya  2569  rgen2a  2587  ralimdva  2600  ralrimiv  2605  r19.21v  2610  ralrimdv  2612  reximdvai  2633  r19.23v  2643  rexlimiv  2645  rexlimdv  2650  r19.29af  2675  r19.29an  2676  r19.29a  2677  r19.32vr  2682  r19.37av  2687  r19.41v  2690  reean  2703  reeanv  2704  cbvrmow  2717  reubidva  2718  rmobidva  2723  cbvralf  2759  cbvrexf  2760  cbvreu  2766  cbvralv  2768  cbvrexv  2769  cbvreuv  2770  cbvrmov  2771  cbvralsv  2784  cbvrexsv  2785  sbralie  2786  cbvrab  2801  cbvrabv  2802  issetf  2811  ceqsalv  2834  ceqsralv  2835  ceqsexv  2843  ceqsex2  2845  ceqsex2v  2846  vtocld  2857  vtocl  2859  vtocl2  2860  vtocl3  2861  vtoclg  2865  vtocl2g  2869  vtoclga  2871  vtocl2gaf  2872  vtocl2ga  2873  vtocl3gaf  2874  vtocl3ga  2875  spcimdv  2891  spcimedv  2893  spcgv  2894  spcegv  2895  rspct  2904  rspc  2905  rspce  2906  rspcv  2907  rspcev  2911  rspc2v  2924  eqvincg  2931  eqvincf  2932  ceqsexgv  2936  elabgt  2948  elab  2951  elabg  2953  elab3g  2958  elrab3t  2962  elrab  2963  ralab2  2971  rexab2  2973  eqeu  2977  mosubt  2984  mo2icl  2986  mob2  2987  mob  2989  reu2  2995  reu3  2997  rmo4f  3005  nfcdeq  3029  sbcco  3054  sbcco2  3055  cbvsbcv  3062  sbcieg  3065  sbcie2g  3066  sbcied  3069  elrabsf  3071  sbcbidv  3091  sbcg  3102  sbc2iegf  3103  sbc2ie  3104  reu8nf  3114  rmo2ilem  3123  rmo3  3125  csbcow  3139  csbeq2dv  3154  nfcsb1d  3159  nfcsbd  3164  csbiebt  3168  csbied  3175  csbie2t  3177  sbcnestg  3182  sbnfc2  3189  cbvralcsf  3191  cbvrexcsf  3192  cbvreucsf  3193  cbvrabcsf  3194  cbvralv2  3195  cbvrexv2  3196  rspc2vd  3197  dfss2f  3219  uniiunlem  3318  abn0m  3522  rabn0m  3524  rabeq0  3526  abeq0  3527  r19.3rmv  3587  r19.28mv  3589  r19.27mv  3593  raaanv  3603  sbss  3604  nfifd  3637  rabsnifsb  3741  euabsn  3745  oprcl  3891  nfuni  3904  nfunid  3905  eluniab  3910  nfint  3943  elintab  3944  iineq2dv  3997  disjiun  4088  opabbidv  4160  nfopab  4162  cbvopab  4165  cbvopabv  4166  cbvopab1  4167  cbvopab2  4168  cbvopab1s  4169  cbvopab1v  4170  mpteq12f  4174  mpteq2dva  4184  cbvmptf  4188  cbvmpt  4189  zfrep6  4211  zfnuleu  4218  intexabim  4247  iinexgm  4249  repizf2  4258  bnd  4268  copsex2t  4343  copsex2g  4344  opelopabsb  4360  opelopabaf  4374  pofun  4415  frind  4455  reusv3  4563  alxfr  4564  rexxfrd  4566  ralxfrALT  4570  onintonm  4621  sucprcreg  4653  eunex  4665  tfis  4687  tfis2  4689  tfisi  4691  peano2  4699  findes  4707  omsinds  4726  opeliunxp  4787  opeliunxp2  4876  ralxpf  4882  rexxpf  4883  dfdmf  4930  reldmm  4956  dfrnf  4979  elrnmpt1  4989  intirr  5130  nfiotadw  5296  cbviota  5298  cbviotav  5300  sb8iota  5301  iota2d  5320  iota2  5323  dffun5r  5345  dffun6f  5346  dffun4f  5349  funco  5373  fun11  5404  imadif  5417  isarep1  5423  isarep2  5424  fun11iun  5613  fv3  5671  tz6.12f  5677  tz6.12c  5678  relelfvdm  5680  nfvres  5684  funimass4  5705  funfvdm2f  5720  fvmptss2  5730  fvmptdf  5743  fvmptdv  5744  fvmptt  5747  eqfnfv2f  5757  ralrnmpt  5797  rexrnmpt  5798  f1ompt  5806  ffnfv  5813  ffnfvf  5814  fmptco  5821  elabrex  5908  elabrexg  5909  dff13f  5921  fliftfun  5947  cbvriota  5993  cbvriotav  5994  riota2  6005  riotaeqimp  6006  riota5f  6008  acexmid  6027  nfoprab  6083  oprabbidv  6085  mpoeq123  6090  cbvoprab1  6103  cbvoprab2  6104  cbvoprab12  6105  cbvoprab12v  6106  cbvoprab3  6107  cbvoprab3v  6108  cbvmpox  6109  ralrnmpo  6146  ovmpodx  6158  ovmpodf  6163  ovmpodv  6164  ovi3  6169  ofrfval2  6261  abrexex2g  6291  opabex3d  6292  opabex3  6293  abrexex2  6295  uchoice  6309  dfoprab4f  6365  fmpox  6374  spc2ed  6407  cnvoprab  6408  f1od2  6409  opeliunxp2f  6447  tposoprab  6489  nfrecs  6516  tfri3  6576  nffrec  6605  eqerlem  6776  erovlem  6839  mptelixpg  6946  dom2lem  6988  modom  7037  xpf1o  7073  mapxpen  7077  nneneq  7086  findcard2  7121  findcard2s  7122  ac6sfi  7130  fiintim  7166  opabfi  7175  exmidomni  7384  fodjuomnilemdc  7386  ismkvnex  7397  mkvprop  7400  exmidfodomrlemr  7456  exmidfodomrlemrALT  7457  cc3  7530  indpi  7605  prarloclem3step  7759  prmuloc2  7830  ltexprlemm  7863  caucvgprprlemaddq  7971  caucvgsrlemgt1  8058  suplocsrlem  8071  axpre-suploclemres  8164  nn0ind-raph  9641  uzind4s  9868  indstr  9871  supinfneg  9873  infsupneg  9874  lbzbi  9894  fzrevral  10385  zsupcllemstep  10535  frecuzrdgtcl  10720  frecuzrdgfunlem  10727  nninfinf  10751  uzsinds  10752  seq3f1olemstep  10822  seq3f1olemp  10823  wrd2ind  11353  reuccatpfxs1  11377  fimaxre2  11850  climeu  11919  nfsum1  11979  nfsum  11980  sumrbdclem  12001  summodclem2a  12005  zsumdc  12008  fsum3  12011  isumss  12015  isumss2  12017  fsum3cvg2  12018  fsumsplitf  12032  fsum2dlemstep  12058  fsum00  12086  fsumrelem  12095  mertenslem2  12160  nfcprod1  12178  nfcprod  12179  prodeq2  12181  prodrbdclem  12195  prodmodclem2a  12200  zproddc  12203  fprodseq  12207  fprodntrivap  12208  prodssdc  12213  fprodcl2lem  12229  fprod2dlemstep  12246  fprodsplitf  12256  fprodsplit1f  12258  fprodap0f  12260  fprodle  12264  divalglemeunn  12545  divalglemeuneg  12547  bezoutlemnewy  12630  bezoutlemmain  12632  bezoutlemzz  12636  bezout  12645  nnwofdc  12672  prmind2  12755  oddpwdclemdvds  12805  oddpwdclemndvds  12806  pcmpt  12979  pcmptdvds  12981  exmidunben  13110  ctiunctlemfo  13123  ctiunct  13124  ctiunctal  13125  dfgrp3mlem  13744  gsumsplit0  13996  lss1d  14462  gsumfzfsumlemm  14666  cnmpt11  15077  cnmpt21  15085  cnmptcom  15092  imasnopn  15093  mulcncf  15402  ellimc3apf  15454  limccnp2cntop  15471  dvmptfsum  15519  lgseisenlem2  15873  gropd  15971  grstructd2dom  15972  ch2varv  16469  elab1  16484  elab2a  16485  elabg2  16486  cbvrald  16489  sumdc2  16500  bdsepnft  16586  bdsepnfALT  16588  bj-omssind  16634  bj-bdfindes  16648  bj-nn0suc0  16649  bj-nntrans  16650  bj-nnelirr  16652  bj-omtrans  16655  setindft  16664  bj-inf2vnlem3  16671  bj-inf2vnlem4  16672  bj-nn0sucALT  16677  bj-findis  16678  bj-findes  16680  strcollnft  16683  strcollnfALT  16685  pw1nct  16708  isomninnlem  16745  trilpolemeq1  16755  trirec0  16759  iswomninnlem  16765  ismkvnnlem  16768  nconstwlpolemgt0  16780  gfsumsn  16797