Theorem nfv 1551

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

Syntax hints:  Ⅎwnf 1483

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 1472  ax-17 1549

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

This theorem is referenced by:  nfvd  1552  alexim  1668  19.37aiv  1698  sbiedv  1812  spimv  1834  spimev  1884  19.36aiv  1925  cbval2  1945  cbvex2  1946  cbval2v  1947  cbvex2v  1948  cbvald  1949  cbvaldva  1952  cbvexdva  1953  eeanv  1960  nfsbv  1975  sbco2h  1992  nfsbt  2004  sbnf2  2009  dfsb7a  2022  sbalyz  2027  sbco4lem  2034  sbco4  2035  dvelimALT  2038  eubidv  2062  sb8eu  2067  nfeudv  2069  nfeud  2070  nfeuv  2072  nfeu  2073  mobidv  2090  mo23  2095  sbmo  2113  mo4  2115  moimv  2120  moanimv  2129  bm1.1  2190  eqsb1lem  2308  eqsb1  2309  clelsb1  2310  clelsb2  2311  abbi  2319  abbidv  2323  cbvabv  2330  clelab  2331  nfcjust  2336  nfcv  2348  clelsb1f  2352  nfeqd  2363  nfeld  2364  nfabdw  2367  nfabd  2368  dvelimdc  2369  cleqf  2373  sbabel  2375  ralbidva  2502  rexbidva  2503  ralbidv  2506  rexbidv  2507  2ralbida  2527  2ralbidva  2528  nfraldya  2541  nfrexdya  2542  rgen2a  2560  ralimdva  2573  ralrimiv  2578  r19.21v  2583  ralrimdv  2585  reximdvai  2606  r19.23v  2615  rexlimiv  2617  rexlimdv  2622  r19.29af  2647  r19.29an  2648  r19.29a  2649  r19.32vr  2654  r19.37av  2659  r19.41v  2662  reean  2675  reeanv  2676  reubidva  2689  rmobidva  2694  cbvralf  2730  cbvrexf  2731  cbvreu  2736  cbvralv  2738  cbvrexv  2739  cbvreuv  2740  cbvrmov  2741  cbvralsv  2754  cbvrexsv  2755  sbralie  2756  cbvrab  2770  cbvrabv  2771  issetf  2779  ceqsalv  2802  ceqsralv  2803  ceqsexv  2811  ceqsex2  2813  ceqsex2v  2814  vtocld  2825  vtocl  2827  vtocl2  2828  vtocl3  2829  vtoclg  2833  vtocl2g  2837  vtoclga  2839  vtocl2gaf  2840  vtocl2ga  2841  vtocl3gaf  2842  vtocl3ga  2843  spcimdv  2857  spcimedv  2859  spcgv  2860  spcegv  2861  rspct  2870  rspc  2871  rspce  2872  rspcv  2873  rspcev  2877  rspc2v  2890  eqvincg  2897  eqvincf  2898  ceqsexgv  2902  elabgt  2914  elab  2917  elabg  2919  elab3g  2924  elrab3t  2928  elrab  2929  ralab2  2937  rexab2  2939  eqeu  2943  mosubt  2950  mo2icl  2952  mob2  2953  mob  2955  reu2  2961  reu3  2963  rmo4f  2971  nfcdeq  2995  sbcco  3020  sbcco2  3021  cbvsbcv  3028  sbcieg  3031  sbcie2g  3032  sbcied  3035  elrabsf  3037  sbcbidv  3057  sbcg  3068  sbc2iegf  3069  sbc2ie  3070  rmo2ilem  3088  rmo3  3090  csbcow  3104  csbeq2dv  3119  nfcsb1d  3124  nfcsbd  3129  csbiebt  3133  csbied  3140  csbie2t  3142  sbcnestg  3147  sbnfc2  3154  cbvralcsf  3156  cbvrexcsf  3157  cbvreucsf  3158  cbvrabcsf  3159  cbvralv2  3160  cbvrexv2  3161  rspc2vd  3162  dfss2f  3184  uniiunlem  3282  abn0m  3486  rabn0m  3488  rabeq0  3490  abeq0  3491  r19.3rmv  3551  r19.28mv  3553  r19.27mv  3557  raaanv  3567  sbss  3568  nfifd  3598  euabsn  3703  oprcl  3843  nfuni  3856  nfunid  3857  eluniab  3862  nfint  3895  elintab  3896  iineq2dv  3949  disjiun  4039  opabbidv  4110  nfopab  4112  cbvopab  4115  cbvopabv  4116  cbvopab1  4117  cbvopab2  4118  cbvopab1s  4119  cbvopab1v  4120  mpteq12f  4124  mpteq2dva  4134  cbvmptf  4138  cbvmpt  4139  zfrep6  4161  zfnuleu  4168  intexabim  4196  iinexgm  4198  repizf2  4206  bnd  4216  copsex2t  4289  copsex2g  4290  opelopabsb  4306  opelopabaf  4320  pofun  4359  frind  4399  reusv3  4507  alxfr  4508  rexxfrd  4510  ralxfrALT  4514  onintonm  4565  sucprcreg  4597  eunex  4609  tfis  4631  tfis2  4633  tfisi  4635  peano2  4643  findes  4651  omsinds  4670  opeliunxp  4730  opeliunxp2  4818  ralxpf  4824  rexxpf  4825  dfdmf  4871  dfrnf  4919  elrnmpt1  4929  intirr  5069  nfiotadw  5235  cbviota  5237  cbviotav  5238  sb8iota  5239  iota2d  5258  iota2  5261  dffun5r  5283  dffun6f  5284  dffun4f  5287  funco  5311  fun11  5341  imadif  5354  isarep1  5360  isarep2  5361  fun11iun  5543  fv3  5599  tz6.12f  5605  tz6.12c  5606  relelfvdm  5608  nfvres  5610  funimass4  5629  funfvdm2f  5644  fvmptss2  5654  fvmptdf  5667  fvmptdv  5668  fvmptt  5671  eqfnfv2f  5681  ralrnmpt  5722  rexrnmpt  5723  f1ompt  5731  ffnfv  5738  ffnfvf  5739  fmptco  5746  elabrex  5826  elabrexg  5827  dff13f  5839  fliftfun  5865  cbvriota  5910  cbvriotav  5911  riota2  5922  riota5f  5924  acexmid  5943  nfoprab  5997  oprabbidv  5999  mpoeq123  6004  cbvoprab1  6017  cbvoprab2  6018  cbvoprab12  6019  cbvoprab12v  6020  cbvoprab3  6021  cbvoprab3v  6022  cbvmpox  6023  ralrnmpo  6060  ovmpodx  6072  ovmpodf  6077  ovmpodv  6078  ovi3  6083  ofrfval2  6175  abrexex2g  6205  opabex3d  6206  opabex3  6207  abrexex2  6209  uchoice  6223  dfoprab4f  6279  fmpox  6286  spc2ed  6319  cnvoprab  6320  f1od2  6321  opeliunxp2f  6324  tposoprab  6366  nfrecs  6393  tfri3  6453  nffrec  6482  eqerlem  6651  erovlem  6714  mptelixpg  6821  dom2lem  6863  xpf1o  6941  mapxpen  6945  nneneq  6954  findcard2  6986  findcard2s  6987  ac6sfi  6995  fiintim  7028  opabfi  7035  exmidomni  7244  fodjuomnilemdc  7246  ismkvnex  7257  mkvprop  7260  exmidfodomrlemr  7310  exmidfodomrlemrALT  7311  cc3  7380  indpi  7455  prarloclem3step  7609  prmuloc2  7680  ltexprlemm  7713  caucvgprprlemaddq  7821  caucvgsrlemgt1  7908  suplocsrlem  7921  axpre-suploclemres  8014  nn0ind-raph  9490  uzind4s  9711  indstr  9714  supinfneg  9716  infsupneg  9717  lbzbi  9737  fzrevral  10227  zsupcllemstep  10372  frecuzrdgtcl  10557  frecuzrdgfunlem  10564  nninfinf  10588  uzsinds  10589  seq3f1olemstep  10659  seq3f1olemp  10660  fimaxre2  11538  climeu  11607  nfsum1  11667  nfsum  11668  sumrbdclem  11688  summodclem2a  11692  zsumdc  11695  fsum3  11698  isumss  11702  isumss2  11704  fsum3cvg2  11705  fsumsplitf  11719  fsum2dlemstep  11745  fsum00  11773  fsumrelem  11782  mertenslem2  11847  nfcprod1  11865  nfcprod  11866  prodeq2  11868  prodrbdclem  11882  prodmodclem2a  11887  zproddc  11890  fprodseq  11894  fprodntrivap  11895  prodssdc  11900  fprodcl2lem  11916  fprod2dlemstep  11933  fprodsplitf  11943  fprodsplit1f  11945  fprodap0f  11947  fprodle  11951  divalglemeunn  12232  divalglemeuneg  12234  bezoutlemnewy  12317  bezoutlemmain  12319  bezoutlemzz  12323  bezout  12332  nnwofdc  12359  prmind2  12442  oddpwdclemdvds  12492  oddpwdclemndvds  12493  pcmpt  12666  pcmptdvds  12668  exmidunben  12797  ctiunctlemfo  12810  ctiunct  12811  ctiunctal  12812  dfgrp3mlem  13430  lss1d  14145  gsumfzfsumlemm  14349  cnmpt11  14755  cnmpt21  14763  cnmptcom  14770  imasnopn  14771  mulcncf  15080  ellimc3apf  15132  limccnp2cntop  15149  dvmptfsum  15197  lgseisenlem2  15548  gropd  15644  grstructd2dom  15645  ch2varv  15704  elab1  15719  elab2a  15720  elabg2  15721  cbvrald  15724  sumdc2  15735  bdsepnft  15823  bdsepnfALT  15825  bj-omssind  15871  bj-bdfindes  15885  bj-nn0suc0  15886  bj-nntrans  15887  bj-nnelirr  15889  bj-omtrans  15892  setindft  15901  bj-inf2vnlem3  15908  bj-inf2vnlem4  15909  bj-nn0sucALT  15914  bj-findis  15915  bj-findes  15917  strcollnft  15920  strcollnfALT  15922  pw1nct  15940  isomninnlem  15969  trilpolemeq1  15979  trirec0  15983  iswomninnlem  15988  ismkvnnlem  15991  nconstwlpolemgt0  16003