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  1838  spimv  1860  spimev  1910  19.36aiv  1953  cbval2  1973  cbvex2  1974  cbval2v  1975  cbvex2v  1976  cbvald  1977  cbvaldva  1980  cbvexdva  1981  eeanv  1988  nfsbv  2003  sbco2h  2020  nfsbt  2032  sbnf2  2037  dfsb7a  2050  sbalyz  2055  sbco4lem  2062  sbco4  2063  dvelimALT  2066  eubidv  2090  sb8eu  2095  nfeudv  2097  nfeud  2098  nfeuv  2100  nfeu  2101  mobidv  2118  mo23  2124  sbmo  2142  mo4  2144  moimv  2149  moanimv  2158  bm1.1  2219  eqsb1lem  2337  eqsb1  2338  clelsb1  2339  clelsb2  2340  abbibcom  2348  abbib  2352  abbidv  2354  cbvabv  2361  clelab  2362  nfcjust  2374  nfcv  2386  clelsb1f  2390  nfeqd  2401  nfeld  2402  nfabdw  2405  nfabd  2406  dvelimdc  2407  cleqf  2411  sbabel  2413  ralbidva  2540  rexbidva  2541  ralbidv  2544  rexbidv  2545  2ralbida  2565  2ralbidva  2566  nfraldya  2579  nfrexdya  2580  rgen2a  2598  ralimdva  2611  ralrimiv  2616  r19.21v  2621  ralrimdv  2623  reximdvai  2644  r19.23v  2654  rexlimiv  2656  rexlimdv  2661  r19.29af  2686  r19.29an  2687  r19.29a  2688  r19.32vr  2693  r19.37av  2698  r19.41v  2701  reean  2714  reeanv  2715  cbvrmow  2729  reubidva  2730  rmobidva  2735  cbvralf  2771  cbvrexf  2772  cbvreu  2778  cbvralv  2780  cbvrexv  2781  cbvreuv  2782  cbvrmov  2783  cbvralsv  2796  cbvrexsv  2797  sbralie  2798  cbvrab  2813  cbvrabv  2814  issetf  2823  ceqsalv  2846  ceqsralv  2847  ceqsexv  2855  ceqsex2  2857  ceqsex2v  2858  vtocld  2869  vtocl  2871  vtocl2  2872  vtocl3  2873  vtoclg  2877  vtocl2g  2881  vtoclga  2883  vtocl2gaf  2884  vtocl2ga  2885  vtocl3gaf  2886  vtocl3ga  2887  spcimdv  2903  spcimedv  2905  spcgv  2906  spcegv  2907  rspct  2916  rspc  2917  rspce  2918  rspcv  2919  rspcev  2923  rspc2v  2937  eqvincg  2944  eqvincf  2945  ceqsexgv  2949  elabgt  2961  elab  2964  elabg  2966  elab3g  2971  elrab3t  2975  elrab  2976  ralab2  2984  rexab2  2986  eqeu  2990  mosubt  2997  mo2icl  2999  mob2  3000  mob  3002  reu2  3008  reu3  3010  rmo4f  3018  nfcdeq  3042  sbcco  3067  sbcco2  3068  cbvsbcv  3075  sbcieg  3078  sbcie2g  3079  sbcied  3082  elrabsf  3084  sbcbidv  3104  sbcg  3115  sbc2iegf  3116  sbc2ie  3117  reu8nf  3127  rmo2ilem  3136  rmo3  3138  csbcow  3152  csbeq2dv  3167  nfcsb1d  3172  nfcsbd  3177  csbiebt  3181  csbied  3188  csbie2t  3190  sbcnestg  3195  sbnfc2  3202  cbvralcsf  3204  cbvrexcsf  3205  cbvreucsf  3206  cbvrabcsf  3207  cbvralv2  3208  cbvrexv2  3209  rspc2vd  3210  dfssf  3232  dfss2f  3233  uniiunlem  3332  abn0m  3538  rabn0m  3540  rabeq0  3542  abeq0  3543  r19.3rmv  3604  r19.28mv  3606  r19.27mv  3610  raaanv  3620  sbss  3621  nfifd  3654  rabsnifsb  3762  euabsn  3766  oprcl  3912  nfuni  3925  nfunid  3926  eluniab  3931  nfint  3964  elintab  3965  iineq2dv  4018  disjiun  4109  opabbidv  4181  nfopab  4183  cbvopab  4186  cbvopabv  4187  cbvopab1  4188  cbvopab2  4189  cbvopab1s  4190  cbvopab1v  4191  mpteq12f  4195  mpteq2dva  4205  cbvmptf  4209  cbvmpt  4210  zfrep6  4232  zfnuleu  4239  intexabim  4269  iinexgm  4271  repizf2  4280  bnd  4290  copsex2t  4366  copsex2g  4367  opelopabsb  4383  opelopabaf  4397  pofun  4438  frind  4478  reusv3  4586  alxfr  4587  rexxfrd  4589  ralxfrALT  4593  onintonm  4644  sucprcreg  4676  eunex  4688  tfis  4710  tfis2  4712  tfisi  4714  peano2  4722  findes  4730  omsinds  4749  opeliunxp  4810  opeliunxp2  4900  ralxpf  4906  rexxpf  4907  dfdmf  4954  reldmm  4980  dfrnf  5003  elrnmpt1  5013  intirr  5154  nfiotadw  5320  cbviota  5322  cbviotav  5324  sb8iota  5325  iota2d  5344  iota2  5347  dffun5r  5369  dffun6f  5370  dffun4f  5373  funco  5397  fun11  5428  imadif  5441  isarep1  5447  isarep2  5448  fun11iun  5640  fv3  5698  tz6.12f  5704  tz6.12c  5705  relelfvdm  5707  nfvres  5711  funimass4  5732  funfvdm2f  5747  fvmptss2  5757  fvmptdf  5770  fvmptdv  5771  fvmptt  5774  eqfnfv2f  5784  ralrnmpt  5824  rexrnmpt  5825  f1ompt  5833  ffnfv  5840  ffnfvf  5841  fmptco  5848  dfimafnf  5928  elabrex  5936  elabrexg  5937  dff13f  5949  fliftfun  5975  cbvriota  6023  cbvriotav  6024  riota2  6035  riotaeqimp  6036  riota5f  6038  acexmid  6057  nfoprab  6113  oprabbidv  6115  mpoeq123  6120  cbvoprab1  6133  cbvoprab2  6134  cbvoprab12  6135  cbvoprab12v  6136  cbvoprab3  6137  cbvoprab3v  6138  cbvmpox  6139  ralrnmpo  6176  ovmpodx  6188  ovmpodf  6193  ovmpodv  6194  ovi3  6199  ofrfval2  6292  abrexex2g  6322  opabex3d  6323  opabex3  6324  abrexex2  6326  elabreximdv  6330  uchoice  6344  dfoprab4f  6400  fmpox  6409  spc2ed  6442  cnvoprab  6443  f1od2  6444  opeliunxp2f  6482  tposoprab  6524  nfrecs  6551  tfri3  6611  nffrec  6640  eqerlem  6811  erovlem  6874  mptelixpg  6982  dom2lem  7024  modom  7074  xpf1o  7110  mapxpen  7114  nneneq  7124  findcard2  7159  findcard2s  7160  ac6sfi  7168  fiintim  7204  opabfi  7213  exmidomni  7446  fodjuomnilemdc  7448  ismkvnex  7459  mkvprop  7462  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  cc3  7598  indpi  7673  prarloclem3step  7827  prmuloc2  7898  ltexprlemm  7931  caucvgprprlemaddq  8039  caucvgsrlemgt1  8126  suplocsrlem  8139  axpre-suploclemres  8232  nn0ind-raph  9713  uzind4s  9940  indstr  9943  supinfneg  9945  infsupneg  9946  lbzbi  9966  fzrevral  10461  zsupcllemstep  10611  frecuzrdgtcl  10798  frecuzrdgfunlem  10805  nninfinf  10829  uzsinds  10830  seq3f1olemstep  10900  seq3f1olemp  10901  wrd2ind  11440  reuccatpfxs1  11464  fimaxre2  11937  climeu  12006  nfsum1  12066  nfsum  12067  sumrbdclem  12088  summodclem2a  12092  zsumdc  12095  fsum3  12098  isumss  12102  isumss2  12104  fsum3cvg2  12105  fsumsplitf  12119  fsum2dlemstep  12145  fsum00  12173  fsumrelem  12182  mertenslem2  12247  nfcprod1  12265  nfcprod  12266  prodeq2  12268  prodrbdclem  12282  prodmodclem2a  12287  zproddc  12290  fprodseq  12294  fprodntrivap  12295  prodssdc  12300  fprodcl2lem  12316  fprod2dlemstep  12333  fprodsplitf  12343  fprodsplit1f  12345  fprodap0f  12347  fprodle  12351  divalglemeunn  12632  divalglemeuneg  12634  bezoutlemnewy  12717  bezoutlemmain  12719  bezoutlemzz  12723  bezout  12732  nnwofdc  12759  prmind2  12842  oddpwdclemdvds  12892  oddpwdclemndvds  12893  pcmpt  13066  pcmptdvds  13068  exmidunben  13261  ctiunctlemfo  13274  ctiunct  13275  ctiunctal  13276  dfgrp3mlem  13853  gsumsplit0  14099  gfsumsn  14107  lss1d  14657  gsumfzfsumlemm  14861  cnmpt11  15274  cnmpt21  15282  cnmptcom  15289  imasnopn  15290  mulcncf  15599  ellimc3apf  15651  limccnp2cntop  15668  dvmptfsum  15716  lgseisenlem2  16070  gropd  16168  grstructd2dom  16169  ch2varv  16666  elab1  16681  elab2a  16682  elabg2  16683  cbvrald  16686  sumdc2  16697  bdsepnft  16783  bdsepnfALT  16785  bj-omssind  16831  bj-bdfindes  16845  bj-nn0suc0  16846  bj-nntrans  16847  bj-nnelirr  16849  bj-omtrans  16852  setindft  16861  bj-inf2vnlem3  16868  bj-inf2vnlem4  16869  bj-nn0sucALT  16874  bj-findis  16875  bj-findes  16877  strcollnft  16880  strcollnfALT  16882  pw1nct  16903  isomninnlem  16940  trilpolemeq1  16950  trirec0  16954  iswomninnlem  16960  ismkvnnlem  16963  nconstwlpolemgt0  16976