Theorem nfv 1552

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

Syntax hints:  Ⅎwnf 1484

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 1473  ax-17 1550

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

This theorem is referenced by:  nfvd  1553  alexim  1669  19.37aiv  1699  sbiedv  1813  spimv  1835  spimev  1885  19.36aiv  1926  cbval2  1946  cbvex2  1947  cbval2v  1948  cbvex2v  1949  cbvald  1950  cbvaldva  1953  cbvexdva  1954  eeanv  1961  nfsbv  1976  sbco2h  1993  nfsbt  2005  sbnf2  2010  dfsb7a  2023  sbalyz  2028  sbco4lem  2035  sbco4  2036  dvelimALT  2039  eubidv  2063  sb8eu  2068  nfeudv  2070  nfeud  2071  nfeuv  2073  nfeu  2074  mobidv  2091  mo23  2097  sbmo  2115  mo4  2117  moimv  2122  moanimv  2131  bm1.1  2192  eqsb1lem  2310  eqsb1  2311  clelsb1  2312  clelsb2  2313  abbi  2321  abbidv  2325  cbvabv  2332  clelab  2333  nfcjust  2338  nfcv  2350  clelsb1f  2354  nfeqd  2365  nfeld  2366  nfabdw  2369  nfabd  2370  dvelimdc  2371  cleqf  2375  sbabel  2377  ralbidva  2504  rexbidva  2505  ralbidv  2508  rexbidv  2509  2ralbida  2529  2ralbidva  2530  nfraldya  2543  nfrexdya  2544  rgen2a  2562  ralimdva  2575  ralrimiv  2580  r19.21v  2585  ralrimdv  2587  reximdvai  2608  r19.23v  2617  rexlimiv  2619  rexlimdv  2624  r19.29af  2649  r19.29an  2650  r19.29a  2651  r19.32vr  2656  r19.37av  2661  r19.41v  2664  reean  2677  reeanv  2678  cbvrmow  2691  reubidva  2692  rmobidva  2697  cbvralf  2733  cbvrexf  2734  cbvreu  2740  cbvralv  2742  cbvrexv  2743  cbvreuv  2744  cbvrmov  2745  cbvralsv  2758  cbvrexsv  2759  sbralie  2760  cbvrab  2774  cbvrabv  2775  issetf  2784  ceqsalv  2807  ceqsralv  2808  ceqsexv  2816  ceqsex2  2818  ceqsex2v  2819  vtocld  2830  vtocl  2832  vtocl2  2833  vtocl3  2834  vtoclg  2838  vtocl2g  2842  vtoclga  2844  vtocl2gaf  2845  vtocl2ga  2846  vtocl3gaf  2847  vtocl3ga  2848  spcimdv  2864  spcimedv  2866  spcgv  2867  spcegv  2868  rspct  2877  rspc  2878  rspce  2879  rspcv  2880  rspcev  2884  rspc2v  2897  eqvincg  2904  eqvincf  2905  ceqsexgv  2909  elabgt  2921  elab  2924  elabg  2926  elab3g  2931  elrab3t  2935  elrab  2936  ralab2  2944  rexab2  2946  eqeu  2950  mosubt  2957  mo2icl  2959  mob2  2960  mob  2962  reu2  2968  reu3  2970  rmo4f  2978  nfcdeq  3002  sbcco  3027  sbcco2  3028  cbvsbcv  3035  sbcieg  3038  sbcie2g  3039  sbcied  3042  elrabsf  3044  sbcbidv  3064  sbcg  3075  sbc2iegf  3076  sbc2ie  3077  reu8nf  3087  rmo2ilem  3096  rmo3  3098  csbcow  3112  csbeq2dv  3127  nfcsb1d  3132  nfcsbd  3137  csbiebt  3141  csbied  3148  csbie2t  3150  sbcnestg  3155  sbnfc2  3162  cbvralcsf  3164  cbvrexcsf  3165  cbvreucsf  3166  cbvrabcsf  3167  cbvralv2  3168  cbvrexv2  3169  rspc2vd  3170  dfss2f  3192  uniiunlem  3290  abn0m  3494  rabn0m  3496  rabeq0  3498  abeq0  3499  r19.3rmv  3559  r19.28mv  3561  r19.27mv  3565  raaanv  3575  sbss  3576  nfifd  3607  euabsn  3713  oprcl  3857  nfuni  3870  nfunid  3871  eluniab  3876  nfint  3909  elintab  3910  iineq2dv  3963  disjiun  4054  opabbidv  4126  nfopab  4128  cbvopab  4131  cbvopabv  4132  cbvopab1  4133  cbvopab2  4134  cbvopab1s  4135  cbvopab1v  4136  mpteq12f  4140  mpteq2dva  4150  cbvmptf  4154  cbvmpt  4155  zfrep6  4177  zfnuleu  4184  intexabim  4212  iinexgm  4214  repizf2  4222  bnd  4232  copsex2t  4307  copsex2g  4308  opelopabsb  4324  opelopabaf  4338  pofun  4377  frind  4417  reusv3  4525  alxfr  4526  rexxfrd  4528  ralxfrALT  4532  onintonm  4583  sucprcreg  4615  eunex  4627  tfis  4649  tfis2  4651  tfisi  4653  peano2  4661  findes  4669  omsinds  4688  opeliunxp  4748  opeliunxp2  4836  ralxpf  4842  rexxpf  4843  dfdmf  4890  dfrnf  4938  elrnmpt1  4948  intirr  5088  nfiotadw  5254  cbviota  5256  cbviotav  5257  sb8iota  5258  iota2d  5277  iota2  5280  dffun5r  5302  dffun6f  5303  dffun4f  5306  funco  5330  fun11  5360  imadif  5373  isarep1  5379  isarep2  5380  fun11iun  5565  fv3  5622  tz6.12f  5628  tz6.12c  5629  relelfvdm  5631  nfvres  5633  funimass4  5652  funfvdm2f  5667  fvmptss2  5677  fvmptdf  5690  fvmptdv  5691  fvmptt  5694  eqfnfv2f  5704  ralrnmpt  5745  rexrnmpt  5746  f1ompt  5754  ffnfv  5761  ffnfvf  5762  fmptco  5769  elabrex  5849  elabrexg  5850  dff13f  5862  fliftfun  5888  cbvriota  5933  cbvriotav  5934  riota2  5945  riota5f  5947  acexmid  5966  nfoprab  6020  oprabbidv  6022  mpoeq123  6027  cbvoprab1  6040  cbvoprab2  6041  cbvoprab12  6042  cbvoprab12v  6043  cbvoprab3  6044  cbvoprab3v  6045  cbvmpox  6046  ralrnmpo  6083  ovmpodx  6095  ovmpodf  6100  ovmpodv  6101  ovi3  6106  ofrfval2  6198  abrexex2g  6228  opabex3d  6229  opabex3  6230  abrexex2  6232  uchoice  6246  dfoprab4f  6302  fmpox  6309  spc2ed  6342  cnvoprab  6343  f1od2  6344  opeliunxp2f  6347  tposoprab  6389  nfrecs  6416  tfri3  6476  nffrec  6505  eqerlem  6674  erovlem  6737  mptelixpg  6844  dom2lem  6886  xpf1o  6966  mapxpen  6970  nneneq  6979  findcard2  7012  findcard2s  7013  ac6sfi  7021  fiintim  7054  opabfi  7061  exmidomni  7270  fodjuomnilemdc  7272  ismkvnex  7283  mkvprop  7286  exmidfodomrlemr  7341  exmidfodomrlemrALT  7342  cc3  7415  indpi  7490  prarloclem3step  7644  prmuloc2  7715  ltexprlemm  7748  caucvgprprlemaddq  7856  caucvgsrlemgt1  7943  suplocsrlem  7956  axpre-suploclemres  8049  nn0ind-raph  9525  uzind4s  9746  indstr  9749  supinfneg  9751  infsupneg  9752  lbzbi  9772  fzrevral  10262  zsupcllemstep  10409  frecuzrdgtcl  10594  frecuzrdgfunlem  10601  nninfinf  10625  uzsinds  10626  seq3f1olemstep  10696  seq3f1olemp  10697  wrd2ind  11214  reuccatpfxs1  11238  fimaxre2  11653  climeu  11722  nfsum1  11782  nfsum  11783  sumrbdclem  11803  summodclem2a  11807  zsumdc  11810  fsum3  11813  isumss  11817  isumss2  11819  fsum3cvg2  11820  fsumsplitf  11834  fsum2dlemstep  11860  fsum00  11888  fsumrelem  11897  mertenslem2  11962  nfcprod1  11980  nfcprod  11981  prodeq2  11983  prodrbdclem  11997  prodmodclem2a  12002  zproddc  12005  fprodseq  12009  fprodntrivap  12010  prodssdc  12015  fprodcl2lem  12031  fprod2dlemstep  12048  fprodsplitf  12058  fprodsplit1f  12060  fprodap0f  12062  fprodle  12066  divalglemeunn  12347  divalglemeuneg  12349  bezoutlemnewy  12432  bezoutlemmain  12434  bezoutlemzz  12438  bezout  12447  nnwofdc  12474  prmind2  12557  oddpwdclemdvds  12607  oddpwdclemndvds  12608  pcmpt  12781  pcmptdvds  12783  exmidunben  12912  ctiunctlemfo  12925  ctiunct  12926  ctiunctal  12927  dfgrp3mlem  13545  lss1d  14260  gsumfzfsumlemm  14464  cnmpt11  14870  cnmpt21  14878  cnmptcom  14885  imasnopn  14886  mulcncf  15195  ellimc3apf  15247  limccnp2cntop  15264  dvmptfsum  15312  lgseisenlem2  15663  gropd  15761  grstructd2dom  15762  ch2varv  15904  elab1  15919  elab2a  15920  elabg2  15921  cbvrald  15924  sumdc2  15935  bdsepnft  16022  bdsepnfALT  16024  bj-omssind  16070  bj-bdfindes  16084  bj-nn0suc0  16085  bj-nntrans  16086  bj-nnelirr  16088  bj-omtrans  16091  setindft  16100  bj-inf2vnlem3  16107  bj-inf2vnlem4  16108  bj-nn0sucALT  16113  bj-findis  16114  bj-findes  16116  strcollnft  16119  strcollnfALT  16121  pw1nct  16142  isomninnlem  16171  trilpolemeq1  16181  trirec0  16185  iswomninnlem  16190  ismkvnnlem  16193  nconstwlpolemgt0  16205