Theorem nfv 1508

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

Syntax hints:  Ⅎwnf 1440

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1429  ax-17 1506

This theorem depends on definitions:  df-bi 116  df-nf 1441

This theorem is referenced by:  nfvd  1509  alexim  1625  19.37aiv  1655  sbiedv  1769  spimv  1791  spimev  1841  19.36aiv  1881  cbval2  1901  cbvex2  1902  cbval2v  1903  cbvex2v  1904  cbvald  1905  cbvaldva  1908  cbvexdva  1909  eeanv  1912  nfsbv  1927  sbco2h  1944  nfsbt  1956  sbnf2  1961  dfsb7a  1974  sbalyz  1979  sbco4lem  1986  sbco4  1987  dvelimALT  1990  eubidv  2014  sb8eu  2019  nfeudv  2021  nfeud  2022  nfeuv  2024  nfeu  2025  mobidv  2042  mo23  2047  sbmo  2065  mo4  2067  moimv  2072  moanimv  2081  bm1.1  2142  eqsb3lem  2260  eqsb3  2261  clelsb3  2262  clelsb4  2263  abbi  2271  abbidv  2275  cbvabv  2282  clelab  2283  nfcjust  2287  nfcv  2299  clelsb3f  2303  nfeqd  2314  nfeld  2315  nfabdw  2318  nfabd  2319  dvelimdc  2320  cleqf  2324  sbabel  2326  ralbidva  2453  rexbidva  2454  ralbidv  2457  rexbidv  2458  2ralbida  2478  2ralbidva  2479  nfraldya  2492  nfrexdya  2493  rgen2a  2511  ralimdva  2524  ralrimiv  2529  r19.21v  2534  ralrimdv  2536  reximdvai  2557  r19.23v  2566  rexlimiv  2568  rexlimdv  2573  r19.29af  2598  r19.29an  2599  r19.29a  2600  r19.32vr  2605  r19.37av  2610  r19.41v  2613  reean  2625  reeanv  2626  reubidva  2639  rmobidva  2644  cbvralf  2674  cbvrexf  2675  cbvreu  2678  cbvralv  2680  cbvrexv  2681  cbvreuv  2682  cbvrmov  2683  cbvralsv  2694  cbvrexsv  2695  sbralie  2696  cbvrab  2710  cbvrabv  2711  issetf  2719  ceqsalv  2742  ceqsralv  2743  ceqsexv  2751  ceqsex2  2752  ceqsex2v  2753  vtocld  2764  vtocl  2766  vtocl2  2767  vtocl3  2768  vtoclg  2772  vtocl2g  2776  vtoclga  2778  vtocl2gaf  2779  vtocl2ga  2780  vtocl3gaf  2781  vtocl3ga  2782  spcimdv  2796  spcimedv  2798  spcgv  2799  spcegv  2800  rspct  2809  rspc  2810  rspce  2811  rspcv  2812  rspcev  2816  rspc2v  2829  eqvincg  2836  eqvincf  2837  ceqsexgv  2841  elabgt  2853  elab  2856  elabg  2858  elab3g  2863  elrab3t  2867  elrab  2868  ralab2  2876  rexab2  2878  eqeu  2882  mosubt  2889  mo2icl  2891  mob2  2892  mob  2894  reu2  2900  reu3  2902  rmo4f  2910  nfcdeq  2934  sbcco  2958  sbcco2  2959  cbvsbcv  2966  sbcieg  2969  sbcie2g  2970  sbcied  2973  elrabsf  2975  sbcbidv  2995  sbcg  3006  sbc2iegf  3007  sbc2ie  3008  rmo2ilem  3026  rmo3  3028  csbcow  3042  csbeq2dv  3057  nfcsb1d  3062  nfcsbd  3066  csbiebt  3070  csbied  3077  csbie2t  3079  sbcnestg  3084  sbnfc2  3091  cbvralcsf  3093  cbvrexcsf  3094  cbvreucsf  3095  cbvrabcsf  3096  cbvralv2  3097  cbvrexv2  3098  dfss2f  3119  uniiunlem  3217  abn0m  3420  rabn0m  3422  rabeq0  3424  abeq0  3425  r19.3rmv  3485  r19.28mv  3487  r19.27mv  3491  raaanv  3502  sbss  3503  nfifd  3533  euabsn  3631  oprcl  3767  nfuni  3780  nfunid  3781  eluniab  3786  nfint  3819  elintab  3820  iineq2dv  3873  disjiun  3962  opabbidv  4032  nfopab  4034  cbvopab  4037  cbvopabv  4038  cbvopab1  4039  cbvopab2  4040  cbvopab1s  4041  cbvopab1v  4042  mpteq12f  4046  mpteq2dva  4056  cbvmptf  4060  cbvmpt  4061  zfrep6  4083  zfnuleu  4090  intexabim  4115  iinexgm  4117  repizf2  4125  bnd  4135  copsex2t  4207  copsex2g  4208  opelopabsb  4222  opelopabaf  4235  pofun  4274  frind  4314  reusv3  4422  alxfr  4423  rexxfrd  4425  ralxfrALT  4429  onintonm  4478  sucprcreg  4510  eunex  4522  tfis  4544  tfis2  4546  tfisi  4548  peano2  4556  findes  4564  omsinds  4583  opeliunxp  4643  opeliunxp2  4728  ralxpf  4734  rexxpf  4735  dfdmf  4781  dfrnf  4829  elrnmpt1  4839  intirr  4974  nfiotadw  5140  cbviota  5142  cbviotav  5143  sb8iota  5144  iota2d  5162  iota2  5163  dffun5r  5184  dffun6f  5185  dffun4f  5188  funco  5212  fun11  5239  imadif  5252  isarep1  5258  isarep2  5259  fun11iun  5437  fv3  5493  tz6.12f  5499  tz6.12c  5500  relelfvdm  5502  nfvres  5503  funimass4  5521  funfvdm2f  5535  fvmptss2  5545  fvmptdf  5557  fvmptdv  5558  fvmptt  5561  eqfnfv2f  5571  ralrnmpt  5611  rexrnmpt  5612  f1ompt  5620  ffnfv  5627  ffnfvf  5628  fmptco  5635  elabrex  5710  dff13f  5722  fliftfun  5748  cbvriota  5792  cbvriotav  5793  riota2  5804  riota5f  5806  acexmid  5825  nfoprab  5875  oprabbidv  5877  mpoeq123  5882  cbvoprab1  5895  cbvoprab2  5896  cbvoprab12  5897  cbvoprab12v  5898  cbvoprab3  5899  cbvoprab3v  5900  cbvmpox  5901  ralrnmpo  5937  ovmpodx  5949  ovmpodf  5954  ovmpodv  5955  ovi3  5959  ofrfval2  6050  abrexex2g  6070  opabex3d  6071  opabex3  6072  abrexex2  6074  dfoprab4f  6143  fmpox  6150  spc2ed  6182  cnvoprab  6183  f1od2  6184  opeliunxp2f  6187  tposoprab  6229  nfrecs  6256  tfri3  6316  nffrec  6345  eqerlem  6513  erovlem  6574  mptelixpg  6681  dom2lem  6719  xpf1o  6791  mapxpen  6795  nneneq  6804  findcard2  6836  findcard2s  6837  ac6sfi  6845  fiintim  6875  exmidomni  7087  fodjuomnilemdc  7089  ismkvnex  7100  mkvprop  7103  exmidfodomrlemr  7139  exmidfodomrlemrALT  7140  cc3  7190  indpi  7264  prarloclem3step  7418  prmuloc2  7489  ltexprlemm  7522  caucvgprprlemaddq  7630  caucvgsrlemgt1  7717  suplocsrlem  7730  axpre-suploclemres  7823  nn0ind-raph  9286  uzind4s  9506  indstr  9509  supinfneg  9511  infsupneg  9512  lbzbi  9531  fzrevral  10013  frecuzrdgtcl  10320  frecuzrdgfunlem  10327  uzsinds  10350  seq3f1olemstep  10409  seq3f1olemp  10410  fimaxre2  11137  climeu  11204  nfsum1  11264  nfsum  11265  sumrbdclem  11285  summodclem2a  11289  zsumdc  11292  fsum3  11295  isumss  11299  isumss2  11301  fsum3cvg2  11302  fsumsplitf  11316  fsum2dlemstep  11342  fsum00  11370  fsumrelem  11379  mertenslem2  11444  nfcprod1  11462  nfcprod  11463  prodeq2  11465  prodrbdclem  11479  prodmodclem2a  11484  zproddc  11487  fprodseq  11491  fprodntrivap  11492  prodssdc  11497  fprodcl2lem  11513  fprod2dlemstep  11530  fprodsplitf  11540  fprodsplit1f  11542  fprodap0f  11544  fprodle  11548  divalglemeunn  11824  divalglemeuneg  11826  zsupcllemstep  11844  bezoutlemnewy  11895  bezoutlemmain  11897  bezoutlemzz  11901  bezout  11910  prmind2  12012  oddpwdclemdvds  12060  oddpwdclemndvds  12061  exmidunben  12225  ctiunctlemfo  12238  ctiunct  12239  ctiunctal  12240  cnmpt11  12753  cnmpt21  12761  cnmptcom  12768  imasnopn  12769  mulcncf  13061  ellimc3apf  13099  limccnp2cntop  13116  ch2varv  13413  elab1  13428  elab2a  13429  elabg2  13430  cbvrald  13433  sumdc2  13444  bdsepnft  13533  bdsepnfALT  13535  bj-omssind  13581  bj-bdfindes  13595  bj-nn0suc0  13596  bj-nntrans  13597  bj-nnelirr  13599  bj-omtrans  13602  setindft  13611  bj-inf2vnlem3  13618  bj-inf2vnlem4  13619  bj-nn0sucALT  13624  bj-findis  13625  bj-findes  13627  strcollnft  13630  strcollnfALT  13632  pw1nct  13646  isomninnlem  13672  trilpolemeq1  13682  trirec0  13686  iswomninnlem  13691  ismkvnnlem  13694  nconstwlpolemgt0  13705