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 1438	1 ⊢ Ⅎ𝑥𝜑

Syntax hints:  Ⅎwnf 1436

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 1425  ax-17 1506

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

This theorem is referenced by:  nfvd  1509  alexim  1624  19.37aiv  1653  sbiedv  1762  spimv  1783  spimev  1833  19.36aiv  1873  cbval2  1893  cbvex2  1894  cbval2v  1895  cbvex2v  1896  cbvald  1897  cbvaldva  1900  cbvexdva  1901  eeanv  1904  sbco2h  1937  nfsbt  1949  sbnf2  1956  dfsb7a  1969  sbalyz  1974  sbco4lem  1981  sbco4  1982  dvelimALT  1985  eubidv  2007  sb8eu  2012  nfeudv  2014  nfeud  2015  nfeuv  2017  nfeu  2018  mobidv  2035  mo23  2040  sbmo  2058  mo4  2060  moimv  2065  moanimv  2074  bm1.1  2124  eqsb3lem  2242  eqsb3  2243  clelsb3  2244  clelsb4  2245  abbi  2253  abbidv  2257  cbvabv  2264  clelab  2265  nfcjust  2269  nfcv  2281  clelsb3f  2285  nfeqd  2296  nfeld  2297  nfabd  2300  dvelimdc  2301  cleqf  2305  sbabel  2307  ralbidva  2433  rexbidva  2434  ralbidv  2437  rexbidv  2438  2ralbida  2456  2ralbidva  2457  nfraldya  2469  nfrexdya  2470  rgen2a  2486  ralimdva  2499  ralrimiv  2504  r19.21v  2509  ralrimdv  2511  reximdvai  2532  r19.23v  2541  rexlimiv  2543  rexlimdv  2548  r19.29af  2573  r19.29an  2574  r19.29a  2575  r19.32vr  2579  r19.37av  2584  r19.41v  2587  reean  2599  reeanv  2600  reubidva  2613  rmobidva  2618  cbvralf  2648  cbvrexf  2649  cbvreu  2652  cbvralv  2654  cbvrexv  2655  cbvreuv  2656  cbvrmov  2657  cbvralsv  2668  cbvrexsv  2669  sbralie  2670  cbvrab  2684  cbvrabv  2685  issetf  2693  ceqsalv  2716  ceqsralv  2717  ceqsexv  2725  ceqsex2  2726  ceqsex2v  2727  vtocld  2738  vtocl  2740  vtocl2  2741  vtocl3  2742  vtoclg  2746  vtocl2g  2750  vtoclga  2752  vtocl2gaf  2753  vtocl2ga  2754  vtocl3gaf  2755  vtocl3ga  2756  spcimdv  2770  spcimedv  2772  spcgv  2773  spcegv  2774  rspct  2782  rspc  2783  rspce  2784  rspcv  2785  rspcev  2789  rspc2v  2802  eqvincg  2809  eqvincf  2810  ceqsexgv  2814  elabgt  2825  elab  2828  elabg  2830  elab3g  2835  elrab3t  2839  elrab  2840  ralab2  2848  rexab2  2850  eqeu  2854  mosubt  2861  mo2icl  2863  mob2  2864  mob  2866  reu2  2872  reu3  2874  rmo4f  2882  nfcdeq  2906  sbcco  2930  sbcco2  2931  cbvsbcv  2938  sbcieg  2941  sbcie2g  2942  sbcied  2945  elrabsf  2947  sbcbidv  2967  sbcg  2978  sbc2iegf  2979  sbc2ie  2980  rmo2ilem  2998  rmo3  3000  csbeq2dv  3028  nfcsb1d  3033  nfcsbd  3036  csbiebt  3039  csbied  3046  csbie2t  3048  sbcnestg  3053  sbnfc2  3060  cbvralcsf  3062  cbvrexcsf  3063  cbvreucsf  3064  cbvrabcsf  3065  cbvralv2  3066  cbvrexv2  3067  dfss2f  3088  uniiunlem  3185  abn0m  3388  rabn0m  3390  rabeq0  3392  abeq0  3393  r19.3rmv  3453  r19.28mv  3455  r19.27mv  3459  raaanv  3470  sbss  3471  nfifd  3499  euabsn  3593  oprcl  3729  nfuni  3742  nfunid  3743  eluniab  3748  nfint  3781  elintab  3782  iineq2dv  3835  disjiun  3924  opabbidv  3994  nfopab  3996  cbvopab  3999  cbvopabv  4000  cbvopab1  4001  cbvopab2  4002  cbvopab1s  4003  cbvopab1v  4004  mpteq12f  4008  mpteq2dva  4018  cbvmptf  4022  cbvmpt  4023  zfrep6  4045  zfnuleu  4052  intexabim  4077  iinexgm  4079  repizf2  4086  bnd  4096  copsex2t  4167  copsex2g  4168  opelopabsb  4182  opelopabaf  4195  pofun  4234  frind  4274  reusv3  4381  alxfr  4382  rexxfrd  4384  ralxfrALT  4388  onintonm  4433  sucprcreg  4464  eunex  4476  tfis  4497  tfis2  4499  tfisi  4501  peano2  4509  findes  4517  omsinds  4535  opeliunxp  4594  opeliunxp2  4679  ralxpf  4685  rexxpf  4686  dfdmf  4732  dfrnf  4780  elrnmpt1  4790  intirr  4925  nfiotadw  5091  cbviota  5093  cbviotav  5094  sb8iota  5095  iota2d  5113  iota2  5114  dffun5r  5135  dffun6f  5136  dffun4f  5139  funco  5163  fun11  5190  imadif  5203  isarep1  5209  isarep2  5210  fun11iun  5388  fv3  5444  tz6.12f  5450  tz6.12c  5451  relelfvdm  5453  nfvres  5454  funimass4  5472  funfvdm2f  5486  fvmptss2  5496  fvmptdf  5508  fvmptdv  5509  fvmptt  5512  eqfnfv2f  5522  ralrnmpt  5562  rexrnmpt  5563  f1ompt  5571  ffnfv  5578  ffnfvf  5579  fmptco  5586  elabrex  5659  dff13f  5671  fliftfun  5697  cbvriota  5740  cbvriotav  5741  riota2  5752  riota5f  5754  acexmid  5773  nfoprab  5823  oprabbidv  5825  mpoeq123  5830  cbvoprab1  5843  cbvoprab2  5844  cbvoprab12  5845  cbvoprab12v  5846  cbvoprab3  5847  cbvoprab3v  5848  cbvmpox  5849  ralrnmpo  5885  ovmpodx  5897  ovmpodf  5902  ovmpodv  5903  ovi3  5907  ofrfval2  5998  abrexex2g  6018  opabex3d  6019  opabex3  6020  abrexex2  6022  dfoprab4f  6091  fmpox  6098  spc2ed  6130  cnvoprab  6131  f1od2  6132  opeliunxp2f  6135  tposoprab  6177  nfrecs  6204  tfri3  6264  nffrec  6293  eqerlem  6460  erovlem  6521  mptelixpg  6628  dom2lem  6666  xpf1o  6738  mapxpen  6742  nneneq  6751  findcard2  6783  findcard2s  6784  ac6sfi  6792  fiintim  6817  exmidomni  7014  fodjuomnilemdc  7016  ismkvnex  7029  mkvprop  7032  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  indpi  7150  prarloclem3step  7304  prmuloc2  7375  ltexprlemm  7408  caucvgprprlemaddq  7516  caucvgsrlemgt1  7603  suplocsrlem  7616  axpre-suploclemres  7709  nn0ind-raph  9168  uzind4s  9385  indstr  9388  supinfneg  9390  infsupneg  9391  lbzbi  9408  fzrevral  9885  frecuzrdgtcl  10185  frecuzrdgfunlem  10192  uzsinds  10215  seq3f1olemstep  10274  seq3f1olemp  10275  fimaxre2  10998  climeu  11065  nfsum1  11125  nfsum  11126  sumrbdclem  11146  summodclem2a  11150  zsumdc  11153  fsum3  11156  isumss  11160  isumss2  11162  fsum3cvg2  11163  fsumsplitf  11177  fsum2dlemstep  11203  fsum00  11231  fsumrelem  11240  mertenslem2  11305  nfcprod1  11323  nfcprod  11324  prodeq2  11326  prodrbdclem  11340  prodmodclem2a  11345  divalglemeunn  11618  divalglemeuneg  11620  zsupcllemstep  11638  bezoutlemnewy  11684  bezoutlemmain  11686  bezoutlemzz  11690  bezout  11699  prmind2  11801  oddpwdclemdvds  11848  oddpwdclemndvds  11849  exmidunben  11939  ctiunctlemfo  11952  ctiunct  11953  cnmpt11  12452  cnmpt21  12460  cnmptcom  12467  imasnopn  12468  mulcncf  12760  ellimc3apf  12798  limccnp2cntop  12815  ch2varv  12975  elab1  12990  elab2a  12991  elabg2  12992  cbvrald  12995  sumdc2  13006  bdsepnft  13085  bdsepnfALT  13087  bj-omssind  13133  bj-bdfindes  13147  bj-nn0suc0  13148  bj-nntrans  13149  bj-nnelirr  13151  bj-omtrans  13154  setindft  13163  bj-inf2vnlem3  13170  bj-inf2vnlem4  13171  bj-nn0sucALT  13176  bj-findis  13177  bj-findes  13179  strcollnft  13182  strcollnfALT  13184  sscoll2  13186  isomninnlem  13225  trilpolemeq1  13233