Theorem nfv 1528

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

Syntax hints:  Ⅎwnf 1460

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 1449  ax-17 1526

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

This theorem is referenced by:  nfvd  1529  alexim  1645  19.37aiv  1675  sbiedv  1789  spimv  1811  spimev  1861  19.36aiv  1901  cbval2  1921  cbvex2  1922  cbval2v  1923  cbvex2v  1924  cbvald  1925  cbvaldva  1928  cbvexdva  1929  eeanv  1932  nfsbv  1947  sbco2h  1964  nfsbt  1976  sbnf2  1981  dfsb7a  1994  sbalyz  1999  sbco4lem  2006  sbco4  2007  dvelimALT  2010  eubidv  2034  sb8eu  2039  nfeudv  2041  nfeud  2042  nfeuv  2044  nfeu  2045  mobidv  2062  mo23  2067  sbmo  2085  mo4  2087  moimv  2092  moanimv  2101  bm1.1  2162  eqsb1lem  2280  eqsb1  2281  clelsb1  2282  clelsb2  2283  abbi  2291  abbidv  2295  cbvabv  2302  clelab  2303  nfcjust  2307  nfcv  2319  clelsb1f  2323  nfeqd  2334  nfeld  2335  nfabdw  2338  nfabd  2339  dvelimdc  2340  cleqf  2344  sbabel  2346  ralbidva  2473  rexbidva  2474  ralbidv  2477  rexbidv  2478  2ralbida  2498  2ralbidva  2499  nfraldya  2512  nfrexdya  2513  rgen2a  2531  ralimdva  2544  ralrimiv  2549  r19.21v  2554  ralrimdv  2556  reximdvai  2577  r19.23v  2586  rexlimiv  2588  rexlimdv  2593  r19.29af  2618  r19.29an  2619  r19.29a  2620  r19.32vr  2625  r19.37av  2630  r19.41v  2633  reean  2646  reeanv  2647  reubidva  2660  rmobidva  2665  cbvralf  2697  cbvrexf  2698  cbvreu  2703  cbvralv  2705  cbvrexv  2706  cbvreuv  2707  cbvrmov  2708  cbvralsv  2721  cbvrexsv  2722  sbralie  2723  cbvrab  2737  cbvrabv  2738  issetf  2746  ceqsalv  2769  ceqsralv  2770  ceqsexv  2778  ceqsex2  2779  ceqsex2v  2780  vtocld  2791  vtocl  2793  vtocl2  2794  vtocl3  2795  vtoclg  2799  vtocl2g  2803  vtoclga  2805  vtocl2gaf  2806  vtocl2ga  2807  vtocl3gaf  2808  vtocl3ga  2809  spcimdv  2823  spcimedv  2825  spcgv  2826  spcegv  2827  rspct  2836  rspc  2837  rspce  2838  rspcv  2839  rspcev  2843  rspc2v  2856  eqvincg  2863  eqvincf  2864  ceqsexgv  2868  elabgt  2880  elab  2883  elabg  2885  elab3g  2890  elrab3t  2894  elrab  2895  ralab2  2903  rexab2  2905  eqeu  2909  mosubt  2916  mo2icl  2918  mob2  2919  mob  2921  reu2  2927  reu3  2929  rmo4f  2937  nfcdeq  2961  sbcco  2986  sbcco2  2987  cbvsbcv  2994  sbcieg  2997  sbcie2g  2998  sbcied  3001  elrabsf  3003  sbcbidv  3023  sbcg  3034  sbc2iegf  3035  sbc2ie  3036  rmo2ilem  3054  rmo3  3056  csbcow  3070  csbeq2dv  3085  nfcsb1d  3090  nfcsbd  3094  csbiebt  3098  csbied  3105  csbie2t  3107  sbcnestg  3112  sbnfc2  3119  cbvralcsf  3121  cbvrexcsf  3122  cbvreucsf  3123  cbvrabcsf  3124  cbvralv2  3125  cbvrexv2  3126  rspc2vd  3127  dfss2f  3148  uniiunlem  3246  abn0m  3450  rabn0m  3452  rabeq0  3454  abeq0  3455  r19.3rmv  3515  r19.28mv  3517  r19.27mv  3521  raaanv  3532  sbss  3533  nfifd  3563  euabsn  3664  oprcl  3804  nfuni  3817  nfunid  3818  eluniab  3823  nfint  3856  elintab  3857  iineq2dv  3910  disjiun  4000  opabbidv  4071  nfopab  4073  cbvopab  4076  cbvopabv  4077  cbvopab1  4078  cbvopab2  4079  cbvopab1s  4080  cbvopab1v  4081  mpteq12f  4085  mpteq2dva  4095  cbvmptf  4099  cbvmpt  4100  zfrep6  4122  zfnuleu  4129  intexabim  4154  iinexgm  4156  repizf2  4164  bnd  4174  copsex2t  4247  copsex2g  4248  opelopabsb  4262  opelopabaf  4275  pofun  4314  frind  4354  reusv3  4462  alxfr  4463  rexxfrd  4465  ralxfrALT  4469  onintonm  4518  sucprcreg  4550  eunex  4562  tfis  4584  tfis2  4586  tfisi  4588  peano2  4596  findes  4604  omsinds  4623  opeliunxp  4683  opeliunxp2  4769  ralxpf  4775  rexxpf  4776  dfdmf  4822  dfrnf  4870  elrnmpt1  4880  intirr  5017  nfiotadw  5183  cbviota  5185  cbviotav  5186  sb8iota  5187  iota2d  5205  iota2  5208  dffun5r  5230  dffun6f  5231  dffun4f  5234  funco  5258  fun11  5285  imadif  5298  isarep1  5304  isarep2  5305  fun11iun  5484  fv3  5540  tz6.12f  5546  tz6.12c  5547  relelfvdm  5549  nfvres  5550  funimass4  5568  funfvdm2f  5583  fvmptss2  5593  fvmptdf  5605  fvmptdv  5606  fvmptt  5609  eqfnfv2f  5619  ralrnmpt  5660  rexrnmpt  5661  f1ompt  5669  ffnfv  5676  ffnfvf  5677  fmptco  5684  elabrex  5760  elabrexg  5761  dff13f  5773  fliftfun  5799  cbvriota  5843  cbvriotav  5844  riota2  5855  riota5f  5857  acexmid  5876  nfoprab  5929  oprabbidv  5931  mpoeq123  5936  cbvoprab1  5949  cbvoprab2  5950  cbvoprab12  5951  cbvoprab12v  5952  cbvoprab3  5953  cbvoprab3v  5954  cbvmpox  5955  ralrnmpo  5991  ovmpodx  6003  ovmpodf  6008  ovmpodv  6009  ovi3  6013  ofrfval2  6101  abrexex2g  6123  opabex3d  6124  opabex3  6125  abrexex2  6127  dfoprab4f  6196  fmpox  6203  spc2ed  6236  cnvoprab  6237  f1od2  6238  opeliunxp2f  6241  tposoprab  6283  nfrecs  6310  tfri3  6370  nffrec  6399  eqerlem  6568  erovlem  6629  mptelixpg  6736  dom2lem  6774  xpf1o  6846  mapxpen  6850  nneneq  6859  findcard2  6891  findcard2s  6892  ac6sfi  6900  fiintim  6930  exmidomni  7142  fodjuomnilemdc  7144  ismkvnex  7155  mkvprop  7158  exmidfodomrlemr  7203  exmidfodomrlemrALT  7204  cc3  7269  indpi  7343  prarloclem3step  7497  prmuloc2  7568  ltexprlemm  7601  caucvgprprlemaddq  7709  caucvgsrlemgt1  7796  suplocsrlem  7809  axpre-suploclemres  7902  nn0ind-raph  9372  uzind4s  9592  indstr  9595  supinfneg  9597  infsupneg  9598  lbzbi  9618  fzrevral  10107  frecuzrdgtcl  10414  frecuzrdgfunlem  10421  uzsinds  10444  seq3f1olemstep  10503  seq3f1olemp  10504  fimaxre2  11237  climeu  11306  nfsum1  11366  nfsum  11367  sumrbdclem  11387  summodclem2a  11391  zsumdc  11394  fsum3  11397  isumss  11401  isumss2  11403  fsum3cvg2  11404  fsumsplitf  11418  fsum2dlemstep  11444  fsum00  11472  fsumrelem  11481  mertenslem2  11546  nfcprod1  11564  nfcprod  11565  prodeq2  11567  prodrbdclem  11581  prodmodclem2a  11586  zproddc  11589  fprodseq  11593  fprodntrivap  11594  prodssdc  11599  fprodcl2lem  11615  fprod2dlemstep  11632  fprodsplitf  11642  fprodsplit1f  11644  fprodap0f  11646  fprodle  11650  divalglemeunn  11928  divalglemeuneg  11930  zsupcllemstep  11948  bezoutlemnewy  11999  bezoutlemmain  12001  bezoutlemzz  12005  bezout  12014  nnwofdc  12041  prmind2  12122  oddpwdclemdvds  12172  oddpwdclemndvds  12173  pcmpt  12343  pcmptdvds  12345  exmidunben  12429  ctiunctlemfo  12442  ctiunct  12443  ctiunctal  12444  dfgrp3mlem  12973  lss1d  13475  cnmpt11  13868  cnmpt21  13876  cnmptcom  13883  imasnopn  13884  mulcncf  14176  ellimc3apf  14214  limccnp2cntop  14231  lgseisenlem2  14536  ch2varv  14605  elab1  14620  elab2a  14621  elabg2  14622  cbvrald  14625  sumdc2  14636  bdsepnft  14724  bdsepnfALT  14726  bj-omssind  14772  bj-bdfindes  14786  bj-nn0suc0  14787  bj-nntrans  14788  bj-nnelirr  14790  bj-omtrans  14793  setindft  14802  bj-inf2vnlem3  14809  bj-inf2vnlem4  14810  bj-nn0sucALT  14815  bj-findis  14816  bj-findes  14818  strcollnft  14821  strcollnfALT  14823  pw1nct  14837  isomninnlem  14863  trilpolemeq1  14873  trirec0  14877  iswomninnlem  14882  ismkvnnlem  14885  nconstwlpolemgt0  14897