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  4198  nfopab  4200  cbvopab  4203  cbvopabv  4204  cbvopab1  4205  cbvopab2  4206  cbvopab1s  4207  cbvopab1v  4208  mpteq12f  4212  mpteq2dva  4223  cbvmptf  4227  cbvmpt  4228  zfrep6  4250  zfnuleu  4259  intexabim  4290  iinexgm  4292  repizf2  4301  bnd  4311  copsex2t  4387  copsex2g  4388  opelopabsb  4404  opelopabaf  4418  pofun  4459  frind  4499  reusv3  4608  alxfr  4609  rexxfrd  4611  ralxfrALT  4615  onintonm  4666  sucprcreg  4698  eunex  4710  tfis  4732  tfis2  4734  tfisi  4736  peano2  4744  findes  4752  omsinds  4771  opeliunxp  4832  opeliunxp2  4922  ralxpf  4928  rexxpf  4929  dfdmf  4976  reldmm  5002  dfrnf  5025  elrnmpt1  5035  intirr  5177  nfiotadw  5343  cbviota  5345  cbviotav  5347  sb8iota  5348  iota2d  5367  iota2  5370  dffun5r  5392  dffun6f  5393  dffun4f  5396  funco  5420  fun11  5451  imadif  5464  isarep1  5470  isarep2  5471  fun11iun  5663  fv3  5721  tz6.12f  5727  tz6.12c  5728  relelfvdm  5730  nfvres  5735  funimass4  5756  funfvdm2f  5771  fvmptss2  5783  fvmptdf  5796  fvmptdv  5797  fvmptt  5800  eqfnfv2f  5813  ralrnmpt  5853  rexrnmpt  5854  f1ompt  5862  ffnfv  5869  ffnfvf  5870  fmptco  5877  dfimafnf  5958  elabrex  5966  elabrexg  5967  dff13f  5979  fliftfun  6005  cbvriota  6053  cbvriotav  6054  riota2  6065  riotaeqimp  6066  riota5f  6068  acexmid  6087  nfoprab  6143  oprabbidv  6145  mpoeq123  6150  cbvoprab1  6163  cbvoprab2  6164  cbvoprab12  6165  cbvoprab12v  6166  cbvoprab3  6167  cbvoprab3v  6168  cbvmpox  6169  ralrnmpo  6206  ovmpodx  6218  ovmpodf  6223  ovmpodv  6224  ovi3  6229  ofrfval2  6323  abrexex2g  6353  opabex3d  6354  opabex3  6355  abrexex2  6357  elabreximdv  6361  uchoice  6375  dfoprab4f  6431  fmpox  6440  spc2ed  6473  cnvoprab  6474  f1od2  6475  opeliunxp2f  6514  tposoprab  6556  nfrecs  6583  tfri3  6643  nffrec  6672  eqerlem  6843  erovlem  6906  mptelixpg  7022  dom2lem  7064  modom  7114  xpf1o  7150  mapxpen  7154  nneneq  7164  findcard2  7199  findcard2s  7200  ac6sfi  7208  fiintim  7244  opabfi  7253  exmidomni  7488  fodjuomnilemdc  7490  ismkvnex  7501  mkvprop  7504  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  cc3  7640  indpi  7715  prarloclem3step  7869  prmuloc2  7940  ltexprlemm  7973  caucvgprprlemaddq  8081  caucvgsrlemgt1  8168  suplocsrlem  8181  axpre-suploclemres  8274  nn0ind-raph  9773  uzind4s  10005  indstr  10008  supinfneg  10010  infsupneg  10011  lbzbi  10031  fzrevral  10528  zsupcllemstep  10678  frecuzrdgtcl  10869  frecuzrdgfunlem  10876  nninfinf  10900  uzsinds  10901  seq3f1olemstep  10971  seq3f1olemp  10972  wrd2ind  11516  reuccatpfxs1  11540  fimaxre2  12015  climeu  12086  nfsum1  12146  nfsum  12147  sumrbdclem  12168  summodclem2a  12172  zsumdc  12175  fsum3  12178  isumss  12182  isumss2  12184  fsum3cvg2  12185  fsumsplitf  12199  fsum2dlemstep  12225  fsum00  12253  fsumrelem  12262  mertenslem2  12327  nfcprod1  12345  nfcprod  12346  prodeq2  12348  prodrbdclem  12362  prodmodclem2a  12367  zproddc  12370  fprodseq  12374  fprodntrivap  12375  prodssdc  12380  fprodcl2lem  12396  fprod2dlemstep  12413  fprodsplitf  12423  fprodsplit1f  12425  fprodap0f  12427  fprodle  12431  divalglemeunn  12712  divalglemeuneg  12714  bezoutlemnewy  12797  bezoutlemmain  12799  bezoutlemzz  12803  bezout  12812  nnwofdc  12839  prmind2  12922  nnmaxpwlemdvds  12973  nnmaxpwlemndvds  12974  pcmpt  13150  pcmptdvds  13152  exmidunben  13374  ctiunctlemfo  13387  ctiunct  13388  ctiunctal  13389  dfgrp3mlem  13961  gzsumsplit0  14237  gsumsncmn  14245  gsumsnfdcmn  14256  gsumsndcmn  14257  gsumunsnfd  14258  gsumcom2fi  14274  lss1d  14828  gsumfsum  15031  cnmpt11  15526  cnmpt21  15534  cnmptcom  15541  imasnopn  15542  mulcncf  15851  ellimc3apf  15903  limccnp2cntop  15920  dvmptfsum  15968  lgseisenlem2  16412  gropd  16510  grstructd2dom  16511  ch2varv  17018  elab1  17033  elab2a  17034  elabg2  17035  cbvrald  17038  sumdc2  17049  bdsepnft  17135  bdsepnfALT  17137  bj-omssind  17183  bj-bdfindes  17197  bj-nn0suc0  17198  bj-nntrans  17199  bj-nnelirr  17201  bj-omtrans  17204  setindft  17213  bj-inf2vnlem3  17220  bj-inf2vnlem4  17221  bj-nn0sucALT  17226  bj-findis  17227  bj-findes  17229  strcollnft  17232  strcollnfALT  17234  pw1nct  17255  isomninnlem  17302  trilpolemeq1  17313  trirec0  17317  iswomninnlem  17323  ismkvnnlem  17326  nconstwlpolemgt0  17338