Theorem nfv 1577

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

Syntax hints:  Ⅎwnf 1509

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 1498  ax-17 1575

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

This theorem is referenced by:  nfvd  1578  alexim  1694  19.37aiv  1723  sbiedv  1838  spimv  1860  spimev  1910  19.36aiv  1951  cbval2  1971  cbvex2  1972  cbval2v  1973  cbvex2v  1974  cbvald  1975  cbvaldva  1978  cbvexdva  1979  eeanv  1986  nfsbv  2001  sbco2h  2018  nfsbt  2030  sbnf2  2035  dfsb7a  2048  sbalyz  2053  sbco4lem  2060  sbco4  2061  dvelimALT  2064  eubidv  2088  sb8eu  2093  nfeudv  2095  nfeud  2096  nfeuv  2098  nfeu  2099  mobidv  2116  mo23  2122  sbmo  2140  mo4  2142  moimv  2147  moanimv  2156  bm1.1  2217  eqsb1lem  2335  eqsb1  2336  clelsb1  2337  clelsb2  2338  abbibcom  2346  abbib  2350  abbidv  2352  cbvabv  2359  clelab  2360  nfcjust  2372  nfcv  2384  clelsb1f  2388  nfeqd  2399  nfeld  2400  nfabdw  2403  nfabd  2404  dvelimdc  2405  cleqf  2409  sbabel  2411  ralbidva  2538  rexbidva  2539  ralbidv  2542  rexbidv  2543  2ralbida  2563  2ralbidva  2564  nfraldya  2577  nfrexdya  2578  rgen2a  2596  ralimdva  2609  ralrimiv  2614  r19.21v  2619  ralrimdv  2621  reximdvai  2642  r19.23v  2652  rexlimiv  2654  rexlimdv  2659  r19.29af  2684  r19.29an  2685  r19.29a  2686  r19.32vr  2691  r19.37av  2696  r19.41v  2699  reean  2712  reeanv  2713  cbvrmow  2727  reubidva  2728  rmobidva  2733  cbvralf  2769  cbvrexf  2770  cbvreu  2776  cbvralv  2778  cbvrexv  2779  cbvreuv  2780  cbvrmov  2781  cbvralsv  2794  cbvrexsv  2795  sbralie  2796  cbvrab  2811  cbvrabv  2812  issetf  2821  ceqsalv  2844  ceqsralv  2845  ceqsexv  2853  ceqsex2  2855  ceqsex2v  2856  vtocld  2867  vtocl  2869  vtocl2  2870  vtocl3  2871  vtoclg  2875  vtocl2g  2879  vtoclga  2881  vtocl2gaf  2882  vtocl2ga  2883  vtocl3gaf  2884  vtocl3ga  2885  spcimdv  2901  spcimedv  2903  spcgv  2904  spcegv  2905  rspct  2914  rspc  2915  rspce  2916  rspcv  2917  rspcev  2921  rspc2v  2934  eqvincg  2941  eqvincf  2942  ceqsexgv  2946  elabgt  2958  elab  2961  elabg  2963  elab3g  2968  elrab3t  2972  elrab  2973  ralab2  2981  rexab2  2983  eqeu  2987  mosubt  2994  mo2icl  2996  mob2  2997  mob  2999  reu2  3005  reu3  3007  rmo4f  3015  nfcdeq  3039  sbcco  3064  sbcco2  3065  cbvsbcv  3072  sbcieg  3075  sbcie2g  3076  sbcied  3079  elrabsf  3081  sbcbidv  3101  sbcg  3112  sbc2iegf  3113  sbc2ie  3114  reu8nf  3124  rmo2ilem  3133  rmo3  3135  csbcow  3149  csbeq2dv  3164  nfcsb1d  3169  nfcsbd  3174  csbiebt  3178  csbied  3185  csbie2t  3187  sbcnestg  3192  sbnfc2  3199  cbvralcsf  3201  cbvrexcsf  3202  cbvreucsf  3203  cbvrabcsf  3204  cbvralv2  3205  cbvrexv2  3206  rspc2vd  3207  dfss2f  3229  uniiunlem  3328  abn0m  3534  rabn0m  3536  rabeq0  3538  abeq0  3539  r19.3rmv  3600  r19.28mv  3602  r19.27mv  3606  raaanv  3616  sbss  3617  nfifd  3650  rabsnifsb  3757  euabsn  3761  oprcl  3907  nfuni  3920  nfunid  3921  eluniab  3926  nfint  3959  elintab  3960  iineq2dv  4013  disjiun  4104  opabbidv  4176  nfopab  4178  cbvopab  4181  cbvopabv  4182  cbvopab1  4183  cbvopab2  4184  cbvopab1s  4185  cbvopab1v  4186  mpteq12f  4190  mpteq2dva  4200  cbvmptf  4204  cbvmpt  4205  zfrep6  4227  zfnuleu  4234  intexabim  4264  iinexgm  4266  repizf2  4275  bnd  4285  copsex2t  4361  copsex2g  4362  opelopabsb  4378  opelopabaf  4392  pofun  4433  frind  4473  reusv3  4581  alxfr  4582  rexxfrd  4584  ralxfrALT  4588  onintonm  4639  sucprcreg  4671  eunex  4683  tfis  4705  tfis2  4707  tfisi  4709  peano2  4717  findes  4725  omsinds  4744  opeliunxp  4805  opeliunxp2  4895  ralxpf  4901  rexxpf  4902  dfdmf  4949  reldmm  4975  dfrnf  4998  elrnmpt1  5008  intirr  5149  nfiotadw  5315  cbviota  5317  cbviotav  5319  sb8iota  5320  iota2d  5339  iota2  5342  dffun5r  5364  dffun6f  5365  dffun4f  5368  funco  5392  fun11  5423  imadif  5436  isarep1  5442  isarep2  5443  fun11iun  5635  fv3  5693  tz6.12f  5699  tz6.12c  5700  relelfvdm  5702  nfvres  5706  funimass4  5727  funfvdm2f  5742  fvmptss2  5752  fvmptdf  5765  fvmptdv  5766  fvmptt  5769  eqfnfv2f  5779  ralrnmpt  5819  rexrnmpt  5820  f1ompt  5828  ffnfv  5835  ffnfvf  5836  fmptco  5843  elabrex  5930  elabrexg  5931  dff13f  5943  fliftfun  5969  cbvriota  6015  cbvriotav  6016  riota2  6027  riotaeqimp  6028  riota5f  6030  acexmid  6049  nfoprab  6105  oprabbidv  6107  mpoeq123  6112  cbvoprab1  6125  cbvoprab2  6126  cbvoprab12  6127  cbvoprab12v  6128  cbvoprab3  6129  cbvoprab3v  6130  cbvmpox  6131  ralrnmpo  6168  ovmpodx  6180  ovmpodf  6185  ovmpodv  6186  ovi3  6191  ofrfval2  6283  abrexex2g  6313  opabex3d  6314  opabex3  6315  abrexex2  6317  uchoice  6331  dfoprab4f  6387  fmpox  6396  spc2ed  6429  cnvoprab  6430  f1od2  6431  opeliunxp2f  6469  tposoprab  6511  nfrecs  6538  tfri3  6598  nffrec  6627  eqerlem  6798  erovlem  6861  mptelixpg  6969  dom2lem  7011  modom  7061  xpf1o  7097  mapxpen  7101  nneneq  7111  findcard2  7146  findcard2s  7147  ac6sfi  7155  fiintim  7191  opabfi  7200  exmidomni  7433  fodjuomnilemdc  7435  ismkvnex  7446  mkvprop  7449  exmidfodomrlemr  7505  exmidfodomrlemrALT  7506  cc3  7582  indpi  7657  prarloclem3step  7811  prmuloc2  7882  ltexprlemm  7915  caucvgprprlemaddq  8023  caucvgsrlemgt1  8110  suplocsrlem  8123  axpre-suploclemres  8216  nn0ind-raph  9695  uzind4s  9922  indstr  9925  supinfneg  9927  infsupneg  9928  lbzbi  9948  fzrevral  10439  zsupcllemstep  10589  frecuzrdgtcl  10774  frecuzrdgfunlem  10781  nninfinf  10805  uzsinds  10806  seq3f1olemstep  10876  seq3f1olemp  10877  wrd2ind  11415  reuccatpfxs1  11439  fimaxre2  11912  climeu  11981  nfsum1  12041  nfsum  12042  sumrbdclem  12063  summodclem2a  12067  zsumdc  12070  fsum3  12073  isumss  12077  isumss2  12079  fsum3cvg2  12080  fsumsplitf  12094  fsum2dlemstep  12120  fsum00  12148  fsumrelem  12157  mertenslem2  12222  nfcprod1  12240  nfcprod  12241  prodeq2  12243  prodrbdclem  12257  prodmodclem2a  12262  zproddc  12265  fprodseq  12269  fprodntrivap  12270  prodssdc  12275  fprodcl2lem  12291  fprod2dlemstep  12308  fprodsplitf  12318  fprodsplit1f  12320  fprodap0f  12322  fprodle  12326  divalglemeunn  12607  divalglemeuneg  12609  bezoutlemnewy  12692  bezoutlemmain  12694  bezoutlemzz  12698  bezout  12707  nnwofdc  12734  prmind2  12817  oddpwdclemdvds  12867  oddpwdclemndvds  12868  pcmpt  13041  pcmptdvds  13043  exmidunben  13177  ctiunctlemfo  13190  ctiunct  13191  ctiunctal  13192  dfgrp3mlem  13811  gsumsplit0  14063  lss1d  14531  gsumfzfsumlemm  14735  cnmpt11  15148  cnmpt21  15156  cnmptcom  15163  imasnopn  15164  mulcncf  15473  ellimc3apf  15525  limccnp2cntop  15542  dvmptfsum  15590  lgseisenlem2  15944  gropd  16042  grstructd2dom  16043  ch2varv  16540  elab1  16555  elab2a  16556  elabg2  16557  cbvrald  16560  sumdc2  16571  bdsepnft  16657  bdsepnfALT  16659  bj-omssind  16705  bj-bdfindes  16719  bj-nn0suc0  16720  bj-nntrans  16721  bj-nnelirr  16723  bj-omtrans  16726  setindft  16735  bj-inf2vnlem3  16742  bj-inf2vnlem4  16743  bj-nn0sucALT  16748  bj-findis  16749  bj-findes  16751  strcollnft  16754  strcollnfALT  16756  pw1nct  16777  isomninnlem  16814  trilpolemeq1  16824  trirec0  16828  iswomninnlem  16834  ismkvnnlem  16837  nconstwlpolemgt0  16850  gfsumsn  16867