Theorem nfv 1574

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

Syntax hints:  Ⅎwnf 1506

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 1495  ax-17 1572

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

This theorem is referenced by:  nfvd  1575  alexim  1691  19.37aiv  1721  sbiedv  1835  spimv  1857  spimev  1907  19.36aiv  1948  cbval2  1968  cbvex2  1969  cbval2v  1970  cbvex2v  1971  cbvald  1972  cbvaldva  1975  cbvexdva  1976  eeanv  1983  nfsbv  1998  sbco2h  2015  nfsbt  2027  sbnf2  2032  dfsb7a  2045  sbalyz  2050  sbco4lem  2057  sbco4  2058  dvelimALT  2061  eubidv  2085  sb8eu  2090  nfeudv  2092  nfeud  2093  nfeuv  2095  nfeu  2096  mobidv  2113  mo23  2119  sbmo  2137  mo4  2139  moimv  2144  moanimv  2153  bm1.1  2214  eqsb1lem  2332  eqsb1  2333  clelsb1  2334  clelsb2  2335  abbi  2343  abbidv  2347  cbvabv  2354  clelab  2355  nfcjust  2360  nfcv  2372  clelsb1f  2376  nfeqd  2387  nfeld  2388  nfabdw  2391  nfabd  2392  dvelimdc  2393  cleqf  2397  sbabel  2399  ralbidva  2526  rexbidva  2527  ralbidv  2530  rexbidv  2531  2ralbida  2551  2ralbidva  2552  nfraldya  2565  nfrexdya  2566  rgen2a  2584  ralimdva  2597  ralrimiv  2602  r19.21v  2607  ralrimdv  2609  reximdvai  2630  r19.23v  2640  rexlimiv  2642  rexlimdv  2647  r19.29af  2672  r19.29an  2673  r19.29a  2674  r19.32vr  2679  r19.37av  2684  r19.41v  2687  reean  2700  reeanv  2701  cbvrmow  2714  reubidva  2715  rmobidva  2720  cbvralf  2756  cbvrexf  2757  cbvreu  2763  cbvralv  2765  cbvrexv  2766  cbvreuv  2767  cbvrmov  2768  cbvralsv  2781  cbvrexsv  2782  sbralie  2783  cbvrab  2797  cbvrabv  2798  issetf  2807  ceqsalv  2830  ceqsralv  2831  ceqsexv  2839  ceqsex2  2841  ceqsex2v  2842  vtocld  2853  vtocl  2855  vtocl2  2856  vtocl3  2857  vtoclg  2861  vtocl2g  2865  vtoclga  2867  vtocl2gaf  2868  vtocl2ga  2869  vtocl3gaf  2870  vtocl3ga  2871  spcimdv  2887  spcimedv  2889  spcgv  2890  spcegv  2891  rspct  2900  rspc  2901  rspce  2902  rspcv  2903  rspcev  2907  rspc2v  2920  eqvincg  2927  eqvincf  2928  ceqsexgv  2932  elabgt  2944  elab  2947  elabg  2949  elab3g  2954  elrab3t  2958  elrab  2959  ralab2  2967  rexab2  2969  eqeu  2973  mosubt  2980  mo2icl  2982  mob2  2983  mob  2985  reu2  2991  reu3  2993  rmo4f  3001  nfcdeq  3025  sbcco  3050  sbcco2  3051  cbvsbcv  3058  sbcieg  3061  sbcie2g  3062  sbcied  3065  elrabsf  3067  sbcbidv  3087  sbcg  3098  sbc2iegf  3099  sbc2ie  3100  reu8nf  3110  rmo2ilem  3119  rmo3  3121  csbcow  3135  csbeq2dv  3150  nfcsb1d  3155  nfcsbd  3160  csbiebt  3164  csbied  3171  csbie2t  3173  sbcnestg  3178  sbnfc2  3185  cbvralcsf  3187  cbvrexcsf  3188  cbvreucsf  3189  cbvrabcsf  3190  cbvralv2  3191  cbvrexv2  3192  rspc2vd  3193  dfss2f  3215  uniiunlem  3313  abn0m  3517  rabn0m  3519  rabeq0  3521  abeq0  3522  r19.3rmv  3582  r19.28mv  3584  r19.27mv  3588  raaanv  3598  sbss  3599  nfifd  3630  euabsn  3736  oprcl  3880  nfuni  3893  nfunid  3894  eluniab  3899  nfint  3932  elintab  3933  iineq2dv  3986  disjiun  4077  opabbidv  4149  nfopab  4151  cbvopab  4154  cbvopabv  4155  cbvopab1  4156  cbvopab2  4157  cbvopab1s  4158  cbvopab1v  4159  mpteq12f  4163  mpteq2dva  4173  cbvmptf  4177  cbvmpt  4178  zfrep6  4200  zfnuleu  4207  intexabim  4235  iinexgm  4237  repizf2  4245  bnd  4255  copsex2t  4330  copsex2g  4331  opelopabsb  4347  opelopabaf  4361  pofun  4402  frind  4442  reusv3  4550  alxfr  4551  rexxfrd  4553  ralxfrALT  4557  onintonm  4608  sucprcreg  4640  eunex  4652  tfis  4674  tfis2  4676  tfisi  4678  peano2  4686  findes  4694  omsinds  4713  opeliunxp  4773  opeliunxp2  4861  ralxpf  4867  rexxpf  4868  dfdmf  4915  reldmm  4941  dfrnf  4964  elrnmpt1  4974  intirr  5114  nfiotadw  5280  cbviota  5282  cbviotav  5284  sb8iota  5285  iota2d  5304  iota2  5307  dffun5r  5329  dffun6f  5330  dffun4f  5333  funco  5357  fun11  5387  imadif  5400  isarep1  5406  isarep2  5407  fun11iun  5592  fv3  5649  tz6.12f  5655  tz6.12c  5656  relelfvdm  5658  nfvres  5662  funimass4  5683  funfvdm2f  5698  fvmptss2  5708  fvmptdf  5721  fvmptdv  5722  fvmptt  5725  eqfnfv2f  5735  ralrnmpt  5776  rexrnmpt  5777  f1ompt  5785  ffnfv  5792  ffnfvf  5793  fmptco  5800  elabrex  5880  elabrexg  5881  dff13f  5893  fliftfun  5919  cbvriota  5965  cbvriotav  5966  riota2  5977  riotaeqimp  5978  riota5f  5980  acexmid  5999  nfoprab  6055  oprabbidv  6057  mpoeq123  6062  cbvoprab1  6075  cbvoprab2  6076  cbvoprab12  6077  cbvoprab12v  6078  cbvoprab3  6079  cbvoprab3v  6080  cbvmpox  6081  ralrnmpo  6118  ovmpodx  6130  ovmpodf  6135  ovmpodv  6136  ovi3  6141  ofrfval2  6233  abrexex2g  6263  opabex3d  6264  opabex3  6265  abrexex2  6267  uchoice  6281  dfoprab4f  6337  fmpox  6344  spc2ed  6377  cnvoprab  6378  f1od2  6379  opeliunxp2f  6382  tposoprab  6424  nfrecs  6451  tfri3  6511  nffrec  6540  eqerlem  6709  erovlem  6772  mptelixpg  6879  dom2lem  6921  xpf1o  7001  mapxpen  7005  nneneq  7014  findcard2  7047  findcard2s  7048  ac6sfi  7056  fiintim  7089  opabfi  7096  exmidomni  7305  fodjuomnilemdc  7307  ismkvnex  7318  mkvprop  7321  exmidfodomrlemr  7376  exmidfodomrlemrALT  7377  cc3  7450  indpi  7525  prarloclem3step  7679  prmuloc2  7750  ltexprlemm  7783  caucvgprprlemaddq  7891  caucvgsrlemgt1  7978  suplocsrlem  7991  axpre-suploclemres  8084  nn0ind-raph  9560  uzind4s  9781  indstr  9784  supinfneg  9786  infsupneg  9787  lbzbi  9807  fzrevral  10297  zsupcllemstep  10444  frecuzrdgtcl  10629  frecuzrdgfunlem  10636  nninfinf  10660  uzsinds  10661  seq3f1olemstep  10731  seq3f1olemp  10732  wrd2ind  11250  reuccatpfxs1  11274  fimaxre2  11733  climeu  11802  nfsum1  11862  nfsum  11863  sumrbdclem  11883  summodclem2a  11887  zsumdc  11890  fsum3  11893  isumss  11897  isumss2  11899  fsum3cvg2  11900  fsumsplitf  11914  fsum2dlemstep  11940  fsum00  11968  fsumrelem  11977  mertenslem2  12042  nfcprod1  12060  nfcprod  12061  prodeq2  12063  prodrbdclem  12077  prodmodclem2a  12082  zproddc  12085  fprodseq  12089  fprodntrivap  12090  prodssdc  12095  fprodcl2lem  12111  fprod2dlemstep  12128  fprodsplitf  12138  fprodsplit1f  12140  fprodap0f  12142  fprodle  12146  divalglemeunn  12427  divalglemeuneg  12429  bezoutlemnewy  12512  bezoutlemmain  12514  bezoutlemzz  12518  bezout  12527  nnwofdc  12554  prmind2  12637  oddpwdclemdvds  12687  oddpwdclemndvds  12688  pcmpt  12861  pcmptdvds  12863  exmidunben  12992  ctiunctlemfo  13005  ctiunct  13006  ctiunctal  13007  dfgrp3mlem  13626  lss1d  14341  gsumfzfsumlemm  14545  cnmpt11  14951  cnmpt21  14959  cnmptcom  14966  imasnopn  14967  mulcncf  15276  ellimc3apf  15328  limccnp2cntop  15345  dvmptfsum  15393  lgseisenlem2  15744  gropd  15842  grstructd2dom  15843  ch2varv  16090  elab1  16105  elab2a  16106  elabg2  16107  cbvrald  16110  sumdc2  16121  bdsepnft  16208  bdsepnfALT  16210  bj-omssind  16256  bj-bdfindes  16270  bj-nn0suc0  16271  bj-nntrans  16272  bj-nnelirr  16274  bj-omtrans  16277  setindft  16286  bj-inf2vnlem3  16293  bj-inf2vnlem4  16294  bj-nn0sucALT  16299  bj-findis  16300  bj-findes  16302  strcollnft  16305  strcollnfALT  16307  pw1nct  16328  isomninnlem  16357  trilpolemeq1  16367  trirec0  16371  iswomninnlem  16376  ismkvnnlem  16379  nconstwlpolemgt0  16391