Theorem nfv 1574

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

Syntax hints:  Ⅎwnf 1506

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 1495  ax-17 1572

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

This theorem is referenced by:  nfvd  1575  alexim  1691  19.37aiv  1721  sbiedv  1835  spimv  1857  spimev  1907  19.36aiv  1948  cbval2  1968  cbvex2  1969  cbval2v  1970  cbvex2v  1971  cbvald  1972  cbvaldva  1975  cbvexdva  1976  eeanv  1983  nfsbv  1998  sbco2h  2015  nfsbt  2027  sbnf2  2032  dfsb7a  2045  sbalyz  2050  sbco4lem  2057  sbco4  2058  dvelimALT  2061  eubidv  2085  sb8eu  2090  nfeudv  2092  nfeud  2093  nfeuv  2095  nfeu  2096  mobidv  2113  mo23  2119  sbmo  2137  mo4  2139  moimv  2144  moanimv  2153  bm1.1  2214  eqsb1lem  2332  eqsb1  2333  clelsb1  2334  clelsb2  2335  abbi  2343  abbidv  2347  cbvabv  2354  clelab  2355  nfcjust  2360  nfcv  2372  clelsb1f  2376  nfeqd  2387  nfeld  2388  nfabdw  2391  nfabd  2392  dvelimdc  2393  cleqf  2397  sbabel  2399  ralbidva  2526  rexbidva  2527  ralbidv  2530  rexbidv  2531  2ralbida  2551  2ralbidva  2552  nfraldya  2565  nfrexdya  2566  rgen2a  2584  ralimdva  2597  ralrimiv  2602  r19.21v  2607  ralrimdv  2609  reximdvai  2630  r19.23v  2640  rexlimiv  2642  rexlimdv  2647  r19.29af  2672  r19.29an  2673  r19.29a  2674  r19.32vr  2679  r19.37av  2684  r19.41v  2687  reean  2700  reeanv  2701  cbvrmow  2714  reubidva  2715  rmobidva  2720  cbvralf  2756  cbvrexf  2757  cbvreu  2763  cbvralv  2765  cbvrexv  2766  cbvreuv  2767  cbvrmov  2768  cbvralsv  2781  cbvrexsv  2782  sbralie  2783  cbvrab  2797  cbvrabv  2798  issetf  2807  ceqsalv  2830  ceqsralv  2831  ceqsexv  2839  ceqsex2  2841  ceqsex2v  2842  vtocld  2853  vtocl  2855  vtocl2  2856  vtocl3  2857  vtoclg  2861  vtocl2g  2865  vtoclga  2867  vtocl2gaf  2868  vtocl2ga  2869  vtocl3gaf  2870  vtocl3ga  2871  spcimdv  2887  spcimedv  2889  spcgv  2890  spcegv  2891  rspct  2900  rspc  2901  rspce  2902  rspcv  2903  rspcev  2907  rspc2v  2920  eqvincg  2927  eqvincf  2928  ceqsexgv  2932  elabgt  2944  elab  2947  elabg  2949  elab3g  2954  elrab3t  2958  elrab  2959  ralab2  2967  rexab2  2969  eqeu  2973  mosubt  2980  mo2icl  2982  mob2  2983  mob  2985  reu2  2991  reu3  2993  rmo4f  3001  nfcdeq  3025  sbcco  3050  sbcco2  3051  cbvsbcv  3058  sbcieg  3061  sbcie2g  3062  sbcied  3065  elrabsf  3067  sbcbidv  3087  sbcg  3098  sbc2iegf  3099  sbc2ie  3100  reu8nf  3110  rmo2ilem  3119  rmo3  3121  csbcow  3135  csbeq2dv  3150  nfcsb1d  3155  nfcsbd  3160  csbiebt  3164  csbied  3171  csbie2t  3173  sbcnestg  3178  sbnfc2  3185  cbvralcsf  3187  cbvrexcsf  3188  cbvreucsf  3189  cbvrabcsf  3190  cbvralv2  3191  cbvrexv2  3192  rspc2vd  3193  dfss2f  3215  uniiunlem  3313  abn0m  3517  rabn0m  3519  rabeq0  3521  abeq0  3522  r19.3rmv  3582  r19.28mv  3584  r19.27mv  3588  raaanv  3598  sbss  3599  nfifd  3630  euabsn  3736  oprcl  3881  nfuni  3894  nfunid  3895  eluniab  3900  nfint  3933  elintab  3934  iineq2dv  3987  disjiun  4078  opabbidv  4150  nfopab  4152  cbvopab  4155  cbvopabv  4156  cbvopab1  4157  cbvopab2  4158  cbvopab1s  4159  cbvopab1v  4160  mpteq12f  4164  mpteq2dva  4174  cbvmptf  4178  cbvmpt  4179  zfrep6  4201  zfnuleu  4208  intexabim  4236  iinexgm  4238  repizf2  4246  bnd  4256  copsex2t  4331  copsex2g  4332  opelopabsb  4348  opelopabaf  4362  pofun  4403  frind  4443  reusv3  4551  alxfr  4552  rexxfrd  4554  ralxfrALT  4558  onintonm  4609  sucprcreg  4641  eunex  4653  tfis  4675  tfis2  4677  tfisi  4679  peano2  4687  findes  4695  omsinds  4714  opeliunxp  4774  opeliunxp2  4862  ralxpf  4868  rexxpf  4869  dfdmf  4916  reldmm  4942  dfrnf  4965  elrnmpt1  4975  intirr  5115  nfiotadw  5281  cbviota  5283  cbviotav  5285  sb8iota  5286  iota2d  5305  iota2  5308  dffun5r  5330  dffun6f  5331  dffun4f  5334  funco  5358  fun11  5388  imadif  5401  isarep1  5407  isarep2  5408  fun11iun  5595  fv3  5652  tz6.12f  5658  tz6.12c  5659  relelfvdm  5661  nfvres  5665  funimass4  5686  funfvdm2f  5701  fvmptss2  5711  fvmptdf  5724  fvmptdv  5725  fvmptt  5728  eqfnfv2f  5738  ralrnmpt  5779  rexrnmpt  5780  f1ompt  5788  ffnfv  5795  ffnfvf  5796  fmptco  5803  elabrex  5887  elabrexg  5888  dff13f  5900  fliftfun  5926  cbvriota  5972  cbvriotav  5973  riota2  5984  riotaeqimp  5985  riota5f  5987  acexmid  6006  nfoprab  6062  oprabbidv  6064  mpoeq123  6069  cbvoprab1  6082  cbvoprab2  6083  cbvoprab12  6084  cbvoprab12v  6085  cbvoprab3  6086  cbvoprab3v  6087  cbvmpox  6088  ralrnmpo  6125  ovmpodx  6137  ovmpodf  6142  ovmpodv  6143  ovi3  6148  ofrfval2  6241  abrexex2g  6271  opabex3d  6272  opabex3  6273  abrexex2  6275  uchoice  6289  dfoprab4f  6345  fmpox  6352  spc2ed  6385  cnvoprab  6386  f1od2  6387  opeliunxp2f  6390  tposoprab  6432  nfrecs  6459  tfri3  6519  nffrec  6548  eqerlem  6719  erovlem  6782  mptelixpg  6889  dom2lem  6931  xpf1o  7013  mapxpen  7017  nneneq  7026  findcard2  7059  findcard2s  7060  ac6sfi  7068  fiintim  7104  opabfi  7111  exmidomni  7320  fodjuomnilemdc  7322  ismkvnex  7333  mkvprop  7336  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  cc3  7465  indpi  7540  prarloclem3step  7694  prmuloc2  7765  ltexprlemm  7798  caucvgprprlemaddq  7906  caucvgsrlemgt1  7993  suplocsrlem  8006  axpre-suploclemres  8099  nn0ind-raph  9575  uzind4s  9797  indstr  9800  supinfneg  9802  infsupneg  9803  lbzbi  9823  fzrevral  10313  zsupcllemstep  10461  frecuzrdgtcl  10646  frecuzrdgfunlem  10653  nninfinf  10677  uzsinds  10678  seq3f1olemstep  10748  seq3f1olemp  10749  wrd2ind  11270  reuccatpfxs1  11294  fimaxre2  11753  climeu  11822  nfsum1  11882  nfsum  11883  sumrbdclem  11903  summodclem2a  11907  zsumdc  11910  fsum3  11913  isumss  11917  isumss2  11919  fsum3cvg2  11920  fsumsplitf  11934  fsum2dlemstep  11960  fsum00  11988  fsumrelem  11997  mertenslem2  12062  nfcprod1  12080  nfcprod  12081  prodeq2  12083  prodrbdclem  12097  prodmodclem2a  12102  zproddc  12105  fprodseq  12109  fprodntrivap  12110  prodssdc  12115  fprodcl2lem  12131  fprod2dlemstep  12148  fprodsplitf  12158  fprodsplit1f  12160  fprodap0f  12162  fprodle  12166  divalglemeunn  12447  divalglemeuneg  12449  bezoutlemnewy  12532  bezoutlemmain  12534  bezoutlemzz  12538  bezout  12547  nnwofdc  12574  prmind2  12657  oddpwdclemdvds  12707  oddpwdclemndvds  12708  pcmpt  12881  pcmptdvds  12883  exmidunben  13012  ctiunctlemfo  13025  ctiunct  13026  ctiunctal  13027  dfgrp3mlem  13646  lss1d  14362  gsumfzfsumlemm  14566  cnmpt11  14972  cnmpt21  14980  cnmptcom  14987  imasnopn  14988  mulcncf  15297  ellimc3apf  15349  limccnp2cntop  15366  dvmptfsum  15414  lgseisenlem2  15765  gropd  15863  grstructd2dom  15864  ch2varv  16187  elab1  16202  elab2a  16203  elabg2  16204  cbvrald  16207  sumdc2  16218  bdsepnft  16305  bdsepnfALT  16307  bj-omssind  16353  bj-bdfindes  16367  bj-nn0suc0  16368  bj-nntrans  16369  bj-nnelirr  16371  bj-omtrans  16374  setindft  16383  bj-inf2vnlem3  16390  bj-inf2vnlem4  16391  bj-nn0sucALT  16396  bj-findis  16397  bj-findes  16399  strcollnft  16402  strcollnfALT  16404  pw1nct  16428  isomninnlem  16458  trilpolemeq1  16468  trirec0  16472  iswomninnlem  16477  ismkvnnlem  16480  nconstwlpolemgt0  16492