Theorem nfv 1581

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

This proof depends on syntax axioms:  Ⅎwnf 1513

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1502  ax-17 1579

This proof depends on definitions:  df-bi 117  df-nf 1514

This theorem is used by:  nfvd  1582  alexim  1698  19.37aiv  1727  sbiedv  1842  spimv  1864  spimev  1914  19.36aiv  1957  cbval2  1977  cbvex2  1978  cbval2v  1979  cbvex2v  1980  cbvald  1981  cbvaldva  1984  cbvexdva  1985  eeanv  1992  nfsbv  2007  sbco2h  2024  nfsbt  2036  sbnf2  2041  dfsb7a  2054  sbalyz  2059  sbco4lem  2066  sbco4  2067  dvelimALT  2070  eubidv  2094  sb8eu  2099  nfeudv  2101  nfeud  2102  nfeuv  2104  nfeu  2105  mobidv  2122  mo23  2128  sbmo  2146  mo4  2148  moimv  2153  moanimv  2162  bm1.1  2223  eqsb1lem  2341  eqsb1  2342  clelsb1  2343  clelsb2  2344  abbibcom  2352  abbib  2356  abbidv  2358  cbvabv  2365  clelab  2366  nfcjust  2380  nfcv  2392  clelsb1f  2396  nfeqd  2407  nfeld  2408  nfabdw  2411  nfabd  2412  dvelimdc  2413  cleqf  2417  sbabel  2419  ralbidva  2546  rexbidva  2547  ralbidv  2550  rexbidv  2551  2ralbida  2571  2ralbidva  2572  nfraldya  2585  nfrexdya  2586  rgen2a  2604  ralimdva  2617  ralrimiv  2622  r19.21v  2627  ralrimdv  2629  reximdvai  2650  r19.23v  2660  rexlimiv  2662  rexlimdv  2667  r19.29af  2692  r19.29an  2693  r19.29a  2694  r19.32vr  2699  r19.37av  2704  r19.41v  2707  reean  2720  reeanv  2721  cbvrmow  2735  reubidva  2736  rmobidva  2741  cbvralf  2777  cbvrexf  2778  cbvreu  2784  cbvralv  2786  cbvrexv  2787  cbvreuv  2788  cbvrmov  2789  cbvralsv  2802  cbvrexsv  2803  sbralie  2804  cbvrab  2819  cbvrabv  2820  issetf  2829  ceqsalv  2852  ceqsralv  2853  ceqsexv  2861  ceqsex2  2863  ceqsex2v  2864  vtocld  2875  vtocl  2877  vtocl2  2878  vtocl3  2879  vtoclg  2883  vtocl2g  2887  vtoclga  2889  vtocl2gaf  2890  vtocl2ga  2891  vtocl3gaf  2892  vtocl3ga  2893  spcimdv  2909  spcimedv  2911  spcgv  2912  spcegv  2913  rspct  2922  rspc  2923  rspce  2924  rspcv  2925  rspcev  2929  rspc2v  2943  eqvincg  2950  eqvincf  2951  ceqsexgv  2955  elabgt  2967  elab  2970  elabg  2972  elab3g  2977  elrab3t  2981  elrab  2982  ralab2  2990  rexab2  2992  eqeu  2996  mosubt  3003  mo2icl  3005  mob2  3006  mob  3008  reu2  3014  reu3  3016  rmo4f  3024  nfcdeq  3048  sbcco  3073  sbcco2  3074  cbvsbcv  3081  sbcieg  3084  sbcie2g  3085  sbcied  3088  elrabsf  3090  sbcbidv  3110  sbcg  3121  sbc2iegf  3122  sbc2ie  3123  reu8nf  3133  rmo2ilem  3142  rmo3  3144  csbcow  3158  csbeq2dv  3173  nfcsb1d  3178  nfcsbd  3183  csbiebt  3187  csbied  3194  csbie2t  3196  sbcnestg  3201  sbnfc2  3208  cbvralcsf  3210  cbvrexcsf  3211  cbvreucsf  3212  cbvrabcsf  3213  cbvralv2  3214  cbvrexv2  3215  rspc2vd  3216  dfssf  3238  dfss2f  3239  uniiunlem  3338  abn0m  3547  rabn0m  3549  rabeq0  3552  abeq0  3553  r19.3rmv  3618  r19.28mv  3620  r19.27mv  3624  raaanv  3634  sbss  3635  nfifd  3668  rabsnifsb  3777  euabsn  3781  oprcl  3928  nfuni  3941  nfunid  3942  eluniab  3947  nfint  3980  elintab  3981  iineq2dv  4034  disjiun  4125  opabbidv  4197  nfopab  4199  cbvopab  4202  cbvopabv  4203  cbvopab1  4204  cbvopab2  4205  cbvopab1s  4206  cbvopab1v  4207  mpteq12f  4211  mpteq2dva  4221  cbvmptf  4225  cbvmpt  4226  zfrep6  4248  zfnuleu  4257  intexabim  4288  iinexgm  4290  repizf2  4299  bnd  4309  copsex2t  4385  copsex2g  4386  opelopabsb  4402  opelopabaf  4416  pofun  4457  frind  4497  reusv3  4606  alxfr  4607  rexxfrd  4609  ralxfrALT  4613  onintonm  4664  sucprcreg  4696  eunex  4708  tfis  4730  tfis2  4732  tfisi  4734  peano2  4742  findes  4750  omsinds  4769  opeliunxp  4830  opeliunxp2  4920  ralxpf  4926  rexxpf  4927  dfdmf  4974  reldmm  5000  dfrnf  5023  elrnmpt1  5033  intirr  5174  nfiotadw  5340  cbviota  5342  cbviotav  5344  sb8iota  5345  iota2d  5364  iota2  5367  dffun5r  5389  dffun6f  5390  dffun4f  5393  funco  5417  fun11  5448  imadif  5461  isarep1  5467  isarep2  5468  fun11iun  5660  fv3  5718  tz6.12f  5724  tz6.12c  5725  relelfvdm  5727  nfvres  5732  funimass4  5753  funfvdm2f  5768  fvmptss2  5780  fvmptdf  5793  fvmptdv  5794  fvmptt  5797  eqfnfv2f  5810  ralrnmpt  5850  rexrnmpt  5851  f1ompt  5859  ffnfv  5866  ffnfvf  5867  fmptco  5874  dfimafnf  5955  elabrex  5963  elabrexg  5964  dff13f  5976  fliftfun  6002  cbvriota  6050  cbvriotav  6051  riota2  6062  riotaeqimp  6063  riota5f  6065  acexmid  6084  nfoprab  6140  oprabbidv  6142  mpoeq123  6147  cbvoprab1  6160  cbvoprab2  6161  cbvoprab12  6162  cbvoprab12v  6163  cbvoprab3  6164  cbvoprab3v  6165  cbvmpox  6166  ralrnmpo  6203  ovmpodx  6215  ovmpodf  6220  ovmpodv  6221  ovi3  6226  ofrfval2  6319  abrexex2g  6349  opabex3d  6350  opabex3  6351  abrexex2  6353  elabreximdv  6357  uchoice  6371  dfoprab4f  6427  fmpox  6436  spc2ed  6469  cnvoprab  6470  f1od2  6471  opeliunxp2f  6509  tposoprab  6551  nfrecs  6578  tfri3  6638  nffrec  6667  eqerlem  6838  erovlem  6901  mptelixpg  7016  dom2lem  7058  modom  7108  xpf1o  7144  mapxpen  7148  nneneq  7158  findcard2  7193  findcard2s  7194  ac6sfi  7202  fiintim  7238  opabfi  7247  exmidomni  7482  fodjuomnilemdc  7484  ismkvnex  7495  mkvprop  7498  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  cc3  7634  indpi  7709  prarloclem3step  7863  prmuloc2  7934  ltexprlemm  7967  caucvgprprlemaddq  8075  caucvgsrlemgt1  8162  suplocsrlem  8175  axpre-suploclemres  8268  nn0ind-raph  9767  uzind4s  9999  indstr  10002  supinfneg  10004  infsupneg  10005  lbzbi  10025  fzrevral  10522  zsupcllemstep  10672  frecuzrdgtcl  10862  frecuzrdgfunlem  10869  nninfinf  10893  uzsinds  10894  seq3f1olemstep  10964  seq3f1olemp  10965  wrd2ind  11509  reuccatpfxs1  11533  fimaxre2  12008  climeu  12078  nfsum1  12138  nfsum  12139  sumrbdclem  12160  summodclem2a  12164  zsumdc  12167  fsum3  12170  isumss  12174  isumss2  12176  fsum3cvg2  12177  fsumsplitf  12191  fsum2dlemstep  12217  fsum00  12245  fsumrelem  12254  mertenslem2  12319  nfcprod1  12337  nfcprod  12338  prodeq2  12340  prodrbdclem  12354  prodmodclem2a  12359  zproddc  12362  fprodseq  12366  fprodntrivap  12367  prodssdc  12372  fprodcl2lem  12388  fprod2dlemstep  12405  fprodsplitf  12415  fprodsplit1f  12417  fprodap0f  12419  fprodle  12423  divalglemeunn  12704  divalglemeuneg  12706  bezoutlemnewy  12789  bezoutlemmain  12791  bezoutlemzz  12795  bezout  12804  nnwofdc  12831  prmind2  12914  nnmaxpwlemdvds  12965  nnmaxpwlemndvds  12966  pcmpt  13142  pcmptdvds  13144  exmidunben  13366  ctiunctlemfo  13379  ctiunct  13380  ctiunctal  13381  dfgrp3mlem  13952  gzsumsplit0  14197  gsumsncmn  14205  lss1d  14769  gsumfsum  14972  cnmpt11  15433  cnmpt21  15441  cnmptcom  15448  imasnopn  15449  mulcncf  15758  ellimc3apf  15810  limccnp2cntop  15827  dvmptfsum  15875  lgseisenlem2  16288  gropd  16386  grstructd2dom  16387  ch2varv  16894  elab1  16909  elab2a  16910  elabg2  16911  cbvrald  16914  sumdc2  16925  bdsepnft  17011  bdsepnfALT  17013  bj-omssind  17059  bj-bdfindes  17073  bj-nn0suc0  17074  bj-nntrans  17075  bj-nnelirr  17077  bj-omtrans  17080  setindft  17089  bj-inf2vnlem3  17096  bj-inf2vnlem4  17097  bj-nn0sucALT  17102  bj-findis  17103  bj-findes  17105  strcollnft  17108  strcollnfALT  17110  pw1nct  17131  isomninnlem  17177  trilpolemeq1  17187  trirec0  17191  iswomninnlem  17197  ismkvnnlem  17200  nconstwlpolemgt0  17212