Theorem nfv 1539

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

Syntax hints:  Ⅎwnf 1471

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 1460  ax-17 1537

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

This theorem is referenced by:  nfvd  1540  alexim  1656  19.37aiv  1686  sbiedv  1800  spimv  1822  spimev  1872  19.36aiv  1913  cbval2  1933  cbvex2  1934  cbval2v  1935  cbvex2v  1936  cbvald  1937  cbvaldva  1940  cbvexdva  1941  eeanv  1948  nfsbv  1963  sbco2h  1980  nfsbt  1992  sbnf2  1997  dfsb7a  2010  sbalyz  2015  sbco4lem  2022  sbco4  2023  dvelimALT  2026  eubidv  2050  sb8eu  2055  nfeudv  2057  nfeud  2058  nfeuv  2060  nfeu  2061  mobidv  2078  mo23  2083  sbmo  2101  mo4  2103  moimv  2108  moanimv  2117  bm1.1  2178  eqsb1lem  2296  eqsb1  2297  clelsb1  2298  clelsb2  2299  abbi  2307  abbidv  2311  cbvabv  2318  clelab  2319  nfcjust  2324  nfcv  2336  clelsb1f  2340  nfeqd  2351  nfeld  2352  nfabdw  2355  nfabd  2356  dvelimdc  2357  cleqf  2361  sbabel  2363  ralbidva  2490  rexbidva  2491  ralbidv  2494  rexbidv  2495  2ralbida  2515  2ralbidva  2516  nfraldya  2529  nfrexdya  2530  rgen2a  2548  ralimdva  2561  ralrimiv  2566  r19.21v  2571  ralrimdv  2573  reximdvai  2594  r19.23v  2603  rexlimiv  2605  rexlimdv  2610  r19.29af  2635  r19.29an  2636  r19.29a  2637  r19.32vr  2642  r19.37av  2647  r19.41v  2650  reean  2663  reeanv  2664  reubidva  2677  rmobidva  2682  cbvralf  2718  cbvrexf  2719  cbvreu  2724  cbvralv  2726  cbvrexv  2727  cbvreuv  2728  cbvrmov  2729  cbvralsv  2742  cbvrexsv  2743  sbralie  2744  cbvrab  2758  cbvrabv  2759  issetf  2767  ceqsalv  2790  ceqsralv  2791  ceqsexv  2799  ceqsex2  2801  ceqsex2v  2802  vtocld  2813  vtocl  2815  vtocl2  2816  vtocl3  2817  vtoclg  2821  vtocl2g  2825  vtoclga  2827  vtocl2gaf  2828  vtocl2ga  2829  vtocl3gaf  2830  vtocl3ga  2831  spcimdv  2845  spcimedv  2847  spcgv  2848  spcegv  2849  rspct  2858  rspc  2859  rspce  2860  rspcv  2861  rspcev  2865  rspc2v  2878  eqvincg  2885  eqvincf  2886  ceqsexgv  2890  elabgt  2902  elab  2905  elabg  2907  elab3g  2912  elrab3t  2916  elrab  2917  ralab2  2925  rexab2  2927  eqeu  2931  mosubt  2938  mo2icl  2940  mob2  2941  mob  2943  reu2  2949  reu3  2951  rmo4f  2959  nfcdeq  2983  sbcco  3008  sbcco2  3009  cbvsbcv  3016  sbcieg  3019  sbcie2g  3020  sbcied  3023  elrabsf  3025  sbcbidv  3045  sbcg  3056  sbc2iegf  3057  sbc2ie  3058  rmo2ilem  3076  rmo3  3078  csbcow  3092  csbeq2dv  3107  nfcsb1d  3112  nfcsbd  3117  csbiebt  3121  csbied  3128  csbie2t  3130  sbcnestg  3135  sbnfc2  3142  cbvralcsf  3144  cbvrexcsf  3145  cbvreucsf  3146  cbvrabcsf  3147  cbvralv2  3148  cbvrexv2  3149  rspc2vd  3150  dfss2f  3171  uniiunlem  3269  abn0m  3473  rabn0m  3475  rabeq0  3477  abeq0  3478  r19.3rmv  3538  r19.28mv  3540  r19.27mv  3544  raaanv  3554  sbss  3555  nfifd  3585  euabsn  3689  oprcl  3829  nfuni  3842  nfunid  3843  eluniab  3848  nfint  3881  elintab  3882  iineq2dv  3935  disjiun  4025  opabbidv  4096  nfopab  4098  cbvopab  4101  cbvopabv  4102  cbvopab1  4103  cbvopab2  4104  cbvopab1s  4105  cbvopab1v  4106  mpteq12f  4110  mpteq2dva  4120  cbvmptf  4124  cbvmpt  4125  zfrep6  4147  zfnuleu  4154  intexabim  4182  iinexgm  4184  repizf2  4192  bnd  4202  copsex2t  4275  copsex2g  4276  opelopabsb  4291  opelopabaf  4305  pofun  4344  frind  4384  reusv3  4492  alxfr  4493  rexxfrd  4495  ralxfrALT  4499  onintonm  4550  sucprcreg  4582  eunex  4594  tfis  4616  tfis2  4618  tfisi  4620  peano2  4628  findes  4636  omsinds  4655  opeliunxp  4715  opeliunxp2  4803  ralxpf  4809  rexxpf  4810  dfdmf  4856  dfrnf  4904  elrnmpt1  4914  intirr  5053  nfiotadw  5219  cbviota  5221  cbviotav  5222  sb8iota  5223  iota2d  5242  iota2  5245  dffun5r  5267  dffun6f  5268  dffun4f  5271  funco  5295  fun11  5322  imadif  5335  isarep1  5341  isarep2  5342  fun11iun  5522  fv3  5578  tz6.12f  5584  tz6.12c  5585  relelfvdm  5587  nfvres  5589  funimass4  5608  funfvdm2f  5623  fvmptss2  5633  fvmptdf  5646  fvmptdv  5647  fvmptt  5650  eqfnfv2f  5660  ralrnmpt  5701  rexrnmpt  5702  f1ompt  5710  ffnfv  5717  ffnfvf  5718  fmptco  5725  elabrex  5801  elabrexg  5802  dff13f  5814  fliftfun  5840  cbvriota  5885  cbvriotav  5886  riota2  5897  riota5f  5899  acexmid  5918  nfoprab  5971  oprabbidv  5973  mpoeq123  5978  cbvoprab1  5991  cbvoprab2  5992  cbvoprab12  5993  cbvoprab12v  5994  cbvoprab3  5995  cbvoprab3v  5996  cbvmpox  5997  ralrnmpo  6034  ovmpodx  6046  ovmpodf  6051  ovmpodv  6052  ovi3  6057  ofrfval2  6149  abrexex2g  6174  opabex3d  6175  opabex3  6176  abrexex2  6178  uchoice  6192  dfoprab4f  6248  fmpox  6255  spc2ed  6288  cnvoprab  6289  f1od2  6290  opeliunxp2f  6293  tposoprab  6335  nfrecs  6362  tfri3  6422  nffrec  6451  eqerlem  6620  erovlem  6683  mptelixpg  6790  dom2lem  6828  xpf1o  6902  mapxpen  6906  nneneq  6915  findcard2  6947  findcard2s  6948  ac6sfi  6956  fiintim  6987  opabfi  6994  exmidomni  7203  fodjuomnilemdc  7205  ismkvnex  7216  mkvprop  7219  exmidfodomrlemr  7264  exmidfodomrlemrALT  7265  cc3  7330  indpi  7404  prarloclem3step  7558  prmuloc2  7629  ltexprlemm  7662  caucvgprprlemaddq  7770  caucvgsrlemgt1  7857  suplocsrlem  7870  axpre-suploclemres  7963  nn0ind-raph  9437  uzind4s  9658  indstr  9661  supinfneg  9663  infsupneg  9664  lbzbi  9684  fzrevral  10174  frecuzrdgtcl  10486  frecuzrdgfunlem  10493  nninfinf  10517  uzsinds  10518  seq3f1olemstep  10588  seq3f1olemp  10589  fimaxre2  11373  climeu  11442  nfsum1  11502  nfsum  11503  sumrbdclem  11523  summodclem2a  11527  zsumdc  11530  fsum3  11533  isumss  11537  isumss2  11539  fsum3cvg2  11540  fsumsplitf  11554  fsum2dlemstep  11580  fsum00  11608  fsumrelem  11617  mertenslem2  11682  nfcprod1  11700  nfcprod  11701  prodeq2  11703  prodrbdclem  11717  prodmodclem2a  11722  zproddc  11725  fprodseq  11729  fprodntrivap  11730  prodssdc  11735  fprodcl2lem  11751  fprod2dlemstep  11768  fprodsplitf  11778  fprodsplit1f  11780  fprodap0f  11782  fprodle  11786  divalglemeunn  12065  divalglemeuneg  12067  zsupcllemstep  12085  bezoutlemnewy  12136  bezoutlemmain  12138  bezoutlemzz  12142  bezout  12151  nnwofdc  12178  prmind2  12261  oddpwdclemdvds  12311  oddpwdclemndvds  12312  pcmpt  12484  pcmptdvds  12486  exmidunben  12586  ctiunctlemfo  12599  ctiunct  12600  ctiunctal  12601  dfgrp3mlem  13173  lss1d  13882  gsumfzfsumlemm  14086  cnmpt11  14462  cnmpt21  14470  cnmptcom  14477  imasnopn  14478  mulcncf  14787  ellimc3apf  14839  limccnp2cntop  14856  dvmptfsum  14904  lgseisenlem2  15228  ch2varv  15330  elab1  15345  elab2a  15346  elabg2  15347  cbvrald  15350  sumdc2  15361  bdsepnft  15449  bdsepnfALT  15451  bj-omssind  15497  bj-bdfindes  15511  bj-nn0suc0  15512  bj-nntrans  15513  bj-nnelirr  15515  bj-omtrans  15518  setindft  15527  bj-inf2vnlem3  15534  bj-inf2vnlem4  15535  bj-nn0sucALT  15540  bj-findis  15541  bj-findes  15543  strcollnft  15546  strcollnfALT  15548  pw1nct  15563  isomninnlem  15590  trilpolemeq1  15600  trirec0  15604  iswomninnlem  15609  ismkvnnlem  15612  nconstwlpolemgt0  15624