Theorem nfv 1418

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 1416	. 2 ⊢ (φ → ∀xφ)
2	1	nfi 1348	1 ⊢ Ⅎxφ

Syntax hints:  Ⅎwnf 1346

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 1335  ax-17 1416

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

This theorem is referenced by:  nfvd  1419  alexim  1533  19.37aiv  1562  sbiedv  1669  spimv  1689  spimev  1738  19.36aiv  1778  cbval2  1793  cbvex2  1794  cbval2v  1795  cbvex2v  1796  cbvald  1797  cbvaldva  1800  cbvexdva  1801  eeanv  1804  sbco2h  1835  nfsbt  1847  sbnf2  1854  dfsb7a  1867  sbalyz  1872  sbco4lem  1879  sbco4  1880  dvelimALT  1883  eubidv  1905  sb8eu  1910  nfeudv  1912  nfeud  1913  nfeuv  1915  nfeu  1916  mobidv  1933  mo23  1938  sbmo  1956  mo4  1958  moimv  1963  moanimv  1972  bm1.1  2022  eqsb3lem  2137  eqsb3  2138  clelsb3  2139  clelsb4  2140  abbi  2148  abbidv  2152  cbvabv  2158  clelab  2159  nfcjust  2163  nfcv  2175  nfeqd  2189  nfeld  2190  nfabd  2193  dvelimdc  2194  cleqf  2198  sbabel  2200  ralbidva  2316  rexbidva  2317  ralbidv  2320  rexbidv  2321  2ralbida  2339  2ralbidva  2340  nfraldya  2352  nfrexdya  2353  rgen2a  2369  ralimdva  2381  ralrimiv  2385  r19.21v  2390  ralrimdv  2392  reximdvai  2413  r19.23v  2419  rexlimiv  2421  rexlimdv  2426  r19.29af  2447  r19.29a  2448  r19.32vr  2452  r19.37av  2457  r19.41v  2460  reean  2472  reeanv  2473  reubidva  2486  rmobidva  2491  cbvralf  2521  cbvrexf  2522  cbvreu  2525  cbvralv  2527  cbvrexv  2528  cbvreuv  2529  cbvrmov  2530  cbvralsv  2538  cbvrexsv  2539  sbralie  2540  cbvrab  2549  cbvrabv  2550  issetf  2556  ceqsalv  2578  ceqsralv  2579  ceqsexv  2587  ceqsex2  2588  ceqsex2v  2589  vtocld  2600  vtocl  2602  vtocl2  2603  vtocl3  2604  vtoclg  2607  vtocl2g  2611  vtoclga  2613  vtocl2gaf  2614  vtocl2ga  2615  vtocl3gaf  2616  vtocl3ga  2617  spcimdv  2631  spcimedv  2633  spcgv  2634  spcegv  2635  rspct  2643  rspc  2644  rspce  2645  rspcv  2646  rspcev  2650  rspc2v  2656  eqvincg  2662  eqvincf  2663  ceqsexgv  2667  elabgt  2678  elab  2681  elabg  2682  elab3g  2687  elrab3t  2691  elrab  2692  ralab2  2699  rexab2  2701  eqeu  2705  mosubt  2712  mo2icl  2714  mob2  2715  mob  2717  reu2  2723  reu3  2725  nfcdeq  2755  sbcco  2779  sbcco2  2780  cbvsbcv  2786  sbcieg  2789  sbcie2g  2790  sbcied  2793  elrabsf  2795  sbcbidv  2811  sbcg  2821  sbc2iegf  2822  sbc2ie  2823  rmo2ilem  2841  rmo3  2843  csbeq2dv  2869  nfcsb1d  2874  nfcsbd  2877  csbiebt  2880  csbied  2886  csbie2t  2888  sbcnestg  2893  sbnfc2  2900  cbvralcsf  2902  cbvrexcsf  2903  cbvreucsf  2904  cbvrabcsf  2905  cbvralv2  2906  cbvrexv2  2907  dfss2f  2930  uniiunlem  3022  rabn0m  3239  rabeq0  3241  abeq0  3242  r19.3rmv  3306  r19.28mv  3308  r19.27mv  3311  raaanv  3322  sbss  3323  nfifd  3349  euabsn  3431  oprcl  3564  nfuni  3577  nfunid  3578  eluniab  3583  nfint  3616  elintab  3617  iineq2dv  3670  opabbidv  3814  nfopab  3816  cbvopab  3819  cbvopabv  3820  cbvopab1  3821  cbvopab2  3822  cbvopab1s  3823  cbvopab1v  3824  mpteq12f  3828  mpteq2dva  3838  cbvmpt  3842  zfrep6  3865  zfnuleu  3872  intexabim  3897  iinexgm  3899  repizf2  3906  bnd  3916  copsex2t  3973  copsex2g  3974  opelopabsb  3988  opelopabaf  4001  pofun  4040  reusv3  4158  alxfr  4159  rexxfrd  4161  ralxfrALT  4165  sucprcreg  4227  eunex  4239  tfis  4249  tfis2  4251  tfisi  4253  peano2  4261  findes  4269  opeliunxp  4338  opeliunxp2  4419  ralxpf  4425  rexxpf  4426  dfdmf  4471  dfrnf  4518  elrnmpt1  4528  intirr  4654  nfiotadxy  4813  cbviota  4815  cbviotav  4816  sb8iota  4817  iota2d  4835  iota2  4836  dffun5r  4857  dffun6f  4858  dffun4f  4861  funco  4883  fun11  4909  imadif  4922  isarep1  4928  isarep2  4929  fun11iun  5090  fv3  5140  tz6.12f  5145  tz6.12c  5146  relelfvdm  5148  nfvres  5149  funimass4  5167  funfvdm2f  5181  fvmptss2  5190  fvmptdf  5201  fvmptdv  5202  fvmptt  5205  eqfnfv2f  5212  ralrnmpt  5252  rexrnmpt  5253  f1ompt  5263  ffnfv  5266  ffnfvf  5267  fmptco  5273  elabrex  5340  dff13f  5352  fliftfun  5379  cbvriota  5421  cbvriotav  5422  riota2  5433  riota5f  5435  acexmid  5454  nfoprab  5499  oprabbidv  5501  mpt2eq123  5506  cbvoprab1  5518  cbvoprab2  5519  cbvoprab12  5520  cbvoprab12v  5521  cbvoprab3  5522  cbvoprab3v  5523  cbvmpt2x  5524  ralrnmpt2  5557  ovmpt2dx  5569  ovmpt2df  5574  ovmpt2dv  5575  ovi3  5579  ofrfval2  5669  abrexex2g  5689  opabex3d  5690  opabex3  5691  abrexex2  5693  dfoprab4f  5761  fmpt2x  5768  tposoprab  5836  nfrecs  5863  tfri3  5894  nffrec  5921  eqerlem  6073  erovlem  6134  dom2lem  6188  indpi  6326  prarloclem3step  6479  prmuloc2  6548  ltexprlemm  6574  nn0ind-raph  8131  uzind4s  8309  indstr  8312  lbzbi  8327  fzrevral  8737  frecuzrdgfn  8879  ch2varv  9243  elab1  9257  elab2a  9258  elabg2  9259  cbvrald  9262  bdsepnft  9342  bdsepnfALT  9344  bj-omssind  9394  bj-bdfindes  9409  bj-nn0suc0  9410  bj-nntrans  9411  bj-nnelirr  9413  bj-omtrans  9416  setindft  9425  bj-inf2vnlem3  9432  bj-inf2vnlem4  9433  bj-nn0sucALT  9438  bj-findis  9439  bj-findes  9441  strcollnft  9444  strcollnfALT  9446  sscoll2  9448