Theorem nfv 1398

Description: If x is not present in φ, then x is not free in φ. (Contributed by Mario Carneiro, 11-Aug-2016.)

Assertion

Ref	Expression
nfv	⊢ Ⅎxφ

Distinct variable group:   φ,x

Proof of Theorem nfv

Step	Hyp	Ref	Expression
1		ax-17 1396	. 2 ⊢ (φ → ∀xφ)
2	1	nfi 1327	1 ⊢ Ⅎxφ

Syntax hints:  Ⅎwnf 1325

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-gen 1314  ax-17 1396

This theorem depends on definitions:  df-bi 110  df-nf 1326

This theorem is referenced by:  nfvd  1399  alexim  1514  19.37aiv  1543  sbiedv  1650  spimv  1670  spimev  1719  19.36aiv  1759  cbval2  1774  cbvex2  1775  cbval2v  1776  cbvex2v  1777  cbvald  1778  cbvaldva  1781  cbvexdva  1782  eeanv  1785  sbco2h  1816  nfsbt  1828  sbnf2  1835  dfsb7a  1848  sbalyz  1853  sbco4lem  1860  sbco4  1861  dvelimALT  1864  eubidv  1886  sb8eu  1891  nfeudv  1893  nfeud  1894  nfeuv  1896  nfeu  1897  mobidv  1914  mo23  1919  sbmo  1937  mo4  1939  moimv  1944  moanimv  1953  bm1.1  2003  eqsb3lem  2118  eqsb3  2119  clelsb3  2120  clelsb4  2121  abbi  2129  abbidv  2133  cbvabv  2139  clelab  2140  nfcjust  2144  nfcv  2156  nfeqd  2170  nfeld  2171  nfabd  2174  dvelimdc  2175  cleqf  2179  sbabel  2181  ralbidva  2296  rexbidva  2297  ralbidv  2300  rexbidv  2301  2ralbida  2319  2ralbidva  2320  nfraldya  2332  nfrexdya  2333  rgen2a  2349  ralimdva  2361  ralrimiv  2365  r19.21v  2370  ralrimdv  2372  reximdvai  2393  r19.23v  2399  rexlimiv  2401  rexlimdv  2406  r19.29af  2427  r19.29a  2428  r19.32vr  2432  r19.37av  2437  r19.41v  2440  reean  2452  reeanv  2453  reubidva  2466  rmobidva  2471  cbvralf  2501  cbvrexf  2502  cbvreu  2505  cbvralv  2507  cbvrexv  2508  cbvreuv  2509  cbvrmov  2510  cbvralsv  2518  cbvrexsv  2519  sbralie  2520  cbvrab  2529  cbvrabv  2530  issetf  2536  ceqsalv  2557  ceqsralv  2558  ceqsexv  2566  ceqsex2  2567  ceqsex2v  2568  vtocld  2579  vtocl  2581  vtocl2  2582  vtocl3  2583  vtoclg  2586  vtocl2g  2590  vtoclga  2592  vtocl2gaf  2593  vtocl2ga  2594  vtocl3gaf  2595  vtocl3ga  2596  spcimdv  2610  spcimedv  2612  spcgv  2613  spcegv  2614  rspct  2622  rspc  2623  rspce  2624  rspcv  2625  rspcev  2629  rspc2v  2635  eqvincg  2641  eqvincf  2642  ceqsexgv  2646  elabgt  2657  elab  2660  elabg  2661  elab3g  2666  elrab3t  2670  elrab  2671  ralab2  2678  rexab2  2680  eqeu  2684  mosubt  2691  mo2icl  2693  mob2  2694  mob  2696  reu2  2702  reu3  2704  nfcdeq  2734  sbcco  2758  sbcco2  2759  cbvsbcv  2765  sbcieg  2768  sbcie2g  2769  sbcied  2772  elrabsf  2774  sbcbidv  2790  sbcg  2800  sbc2iegf  2801  sbc2ie  2802  rmo2ilem  2820  rmo3  2822  csbeq2dv  2848  nfcsb1d  2853  nfcsbd  2856  csbiebt  2859  csbied  2865  csbie2t  2867  sbcnestg  2872  sbnfc2  2879  cbvralcsf  2881  cbvrexcsf  2882  cbvreucsf  2883  cbvrabcsf  2884  cbvralv2  2885  cbvrexv2  2886  dfss2f  2909  uniiunlem  3001  rabn0m  3218  rabeq0  3220  abeq0  3221  r19.3rmv  3286  r19.28mv  3289  r19.27mv  3292  raaanv  3303  sbss  3304  nfifd  3328  euabsn  3410  oprcl  3543  nfuni  3556  nfunid  3557  eluniab  3562  nfint  3595  elintab  3596  iineq2dv  3649  opabbidv  3793  nfopab  3795  cbvopab  3798  cbvopabv  3799  cbvopab1  3800  cbvopab2  3801  cbvopab1s  3802  cbvopab1v  3803  mpteq12f  3807  mpteq2dva  3817  cbvmpt  3821  zfrep6  3844  zfnuleu  3851  intexabim  3876  iinexgm  3878  repizf2  3885  bnd  3895  copsex2t  3952  copsex2g  3953  opelopabsb  3967  opelopabaf  3980  pofun  4019  reusv3  4138  alxfr  4139  rexxfrd  4141  ralxfrALT  4145  sucprcreg  4207  eunex  4219  tfis  4229  tfis2  4231  tfisi  4233  peano2  4241  findes  4249  opeliunxp  4318  opeliunxp2  4399  ralxpf  4405  rexxpf  4406  dfdmf  4451  dfrnf  4498  elrnmpt1  4508  intirr  4634  nfiotadxy  4793  cbviota  4795  cbviotav  4796  sb8iota  4797  iota2d  4815  iota2  4816  dffun6f  4837  dffun4f  4840  funco  4862  fun11  4888  imadif  4901  isarep1  4907  isarep2  4908  fun11iun  5068  fv3  5118  tz6.12f  5123  tz6.12c  5124  relelfvdm  5126  nfvres  5127  funimass4  5145  funfvdm2f  5159  fvmptss2  5168  fvmptdf  5179  fvmptdv  5180  fvmptt  5183  eqfnfv2f  5190  ralrnmpt  5230  rexrnmpt  5231  f1ompt  5241  ffnfv  5244  ffnfvf  5245  fmptco  5251  elabrex  5318  dff13f  5330  fliftfun  5357  cbvriota  5398  cbvriotav  5399  riota2  5410  riota5f  5412  acexmid  5431  nfoprab  5476  oprabbidv  5478  mpt2eq123  5483  cbvoprab1  5495  cbvoprab2  5496  cbvoprab12  5497  cbvoprab12v  5498  cbvoprab3  5499  cbvoprab3v  5500  cbvmpt2x  5501  ralrnmpt2  5534  ovmpt2dx  5546  ovmpt2df  5551  ovmpt2dv  5552  ovi3  5556  ofrfval2  5646  abrexex2g  5666  opabex3d  5667  opabex3  5668  abrexex2  5670  dfoprab4f  5738  fmpt2x  5745  tposoprab  5813  nfrecs  5840  tfri3  5871  eqerlem  6044  erovlem  6105  prarloclem3step  6344  prmuloc2  6405  ltexprlemm  6431  ch2varv  7154  elab1  7168  elab2a  7169  elabg2  7170  cbvrald  7173  bdsepnft  7252  bdsepnfALT  7254  bj-omssind  7296  bj-bdfindes  7310  bj-nn0suc0  7311  bj-nntrans  7312  bj-nnelirr  7314  bj-omtrans  7317  setindft  7322  bj-inf2vnlem3  7329  bj-inf2vnlem4  7330  bj-nn0sucALT  7335  bj-findis  7336  bj-findes  7338  strcollnft  7341  strcollnfALT  7343  sscoll2  7345