Theorem nfv 1421

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

Syntax hints:  Ⅎwnf 1349

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-gen 1338  ax-17 1419

This theorem depends on definitions:  df-bi 110  df-nf 1350

This theorem is referenced by:  nfvd  1422  alexim  1536  19.37aiv  1565  sbiedv  1672  spimv  1692  spimev  1741  19.36aiv  1781  cbval2  1796  cbvex2  1797  cbval2v  1798  cbvex2v  1799  cbvald  1800  cbvaldva  1803  cbvexdva  1804  eeanv  1807  sbco2h  1838  nfsbt  1850  sbnf2  1857  dfsb7a  1870  sbalyz  1875  sbco4lem  1882  sbco4  1883  dvelimALT  1886  eubidv  1908  sb8eu  1913  nfeudv  1915  nfeud  1916  nfeuv  1918  nfeu  1919  mobidv  1936  mo23  1941  sbmo  1959  mo4  1961  moimv  1966  moanimv  1975  bm1.1  2025  eqsb3lem  2140  eqsb3  2141  clelsb3  2142  clelsb4  2143  abbi  2151  abbidv  2155  cbvabv  2161  clelab  2162  nfcjust  2166  nfcv  2178  nfeqd  2192  nfeld  2193  nfabd  2196  dvelimdc  2197  cleqf  2201  sbabel  2203  ralbidva  2322  rexbidva  2323  ralbidv  2326  rexbidv  2327  2ralbida  2345  2ralbidva  2346  nfraldya  2358  nfrexdya  2359  rgen2a  2375  ralimdva  2387  ralrimiv  2391  r19.21v  2396  ralrimdv  2398  reximdvai  2419  r19.23v  2425  rexlimiv  2427  rexlimdv  2432  r19.29af  2453  r19.29a  2454  r19.32vr  2458  r19.37av  2463  r19.41v  2466  reean  2478  reeanv  2479  reubidva  2492  rmobidva  2497  cbvralf  2527  cbvrexf  2528  cbvreu  2531  cbvralv  2533  cbvrexv  2534  cbvreuv  2535  cbvrmov  2536  cbvralsv  2544  cbvrexsv  2545  sbralie  2546  cbvrab  2555  cbvrabv  2556  issetf  2562  ceqsalv  2584  ceqsralv  2585  ceqsexv  2593  ceqsex2  2594  ceqsex2v  2595  vtocld  2606  vtocl  2608  vtocl2  2609  vtocl3  2610  vtoclg  2613  vtocl2g  2617  vtoclga  2619  vtocl2gaf  2620  vtocl2ga  2621  vtocl3gaf  2622  vtocl3ga  2623  spcimdv  2637  spcimedv  2639  spcgv  2640  spcegv  2641  rspct  2649  rspc  2650  rspce  2651  rspcv  2652  rspcev  2656  rspc2v  2662  eqvincg  2668  eqvincf  2669  ceqsexgv  2673  elabgt  2684  elab  2687  elabg  2688  elab3g  2693  elrab3t  2697  elrab  2698  ralab2  2705  rexab2  2707  eqeu  2711  mosubt  2718  mo2icl  2720  mob2  2721  mob  2723  reu2  2729  reu3  2731  nfcdeq  2761  sbcco  2785  sbcco2  2786  cbvsbcv  2792  sbcieg  2795  sbcie2g  2796  sbcied  2799  elrabsf  2801  sbcbidv  2817  sbcg  2827  sbc2iegf  2828  sbc2ie  2829  rmo2ilem  2847  rmo3  2849  csbeq2dv  2875  nfcsb1d  2880  nfcsbd  2883  csbiebt  2886  csbied  2892  csbie2t  2894  sbcnestg  2899  sbnfc2  2906  cbvralcsf  2908  cbvrexcsf  2909  cbvreucsf  2910  cbvrabcsf  2911  cbvralv2  2912  cbvrexv2  2913  dfss2f  2936  uniiunlem  3028  rabn0m  3245  rabeq0  3247  abeq0  3248  r19.3rmv  3312  r19.28mv  3314  r19.27mv  3317  raaanv  3328  sbss  3329  nfifd  3355  euabsn  3440  oprcl  3573  nfuni  3586  nfunid  3587  eluniab  3592  nfint  3625  elintab  3626  iineq2dv  3679  opabbidv  3823  nfopab  3825  cbvopab  3828  cbvopabv  3829  cbvopab1  3830  cbvopab2  3831  cbvopab1s  3832  cbvopab1v  3833  mpteq12f  3837  mpteq2dva  3847  cbvmpt  3851  zfrep6  3874  zfnuleu  3881  intexabim  3906  iinexgm  3908  repizf2  3915  bnd  3925  copsex2t  3982  copsex2g  3983  opelopabsb  3997  opelopabaf  4010  pofun  4049  frind  4089  reusv3  4192  alxfr  4193  rexxfrd  4195  ralxfrALT  4199  onintonm  4243  sucprcreg  4273  eunex  4285  tfis  4306  tfis2  4308  tfisi  4310  peano2  4318  findes  4326  opeliunxp  4395  opeliunxp2  4476  ralxpf  4482  rexxpf  4483  dfdmf  4528  dfrnf  4575  elrnmpt1  4585  intirr  4711  nfiotadxy  4870  cbviota  4872  cbviotav  4873  sb8iota  4874  iota2d  4892  iota2  4893  dffun5r  4914  dffun6f  4915  dffun4f  4918  funco  4940  fun11  4966  imadif  4979  isarep1  4985  isarep2  4986  fun11iun  5147  fv3  5197  tz6.12f  5202  tz6.12c  5203  relelfvdm  5205  nfvres  5206  funimass4  5224  funfvdm2f  5238  fvmptss2  5247  fvmptdf  5258  fvmptdv  5259  fvmptt  5262  eqfnfv2f  5269  ralrnmpt  5309  rexrnmpt  5310  f1ompt  5320  ffnfv  5323  ffnfvf  5324  fmptco  5330  elabrex  5397  dff13f  5409  fliftfun  5436  cbvriota  5478  cbvriotav  5479  riota2  5490  riota5f  5492  acexmid  5511  nfoprab  5557  oprabbidv  5559  mpt2eq123  5564  cbvoprab1  5576  cbvoprab2  5577  cbvoprab12  5578  cbvoprab12v  5579  cbvoprab3  5580  cbvoprab3v  5581  cbvmpt2x  5582  ralrnmpt2  5615  ovmpt2dx  5627  ovmpt2df  5632  ovmpt2dv  5633  ovi3  5637  ofrfval2  5727  abrexex2g  5747  opabex3d  5748  opabex3  5749  abrexex2  5751  dfoprab4f  5819  fmpt2x  5826  tposoprab  5895  nfrecs  5922  tfri3  5953  nffrec  5982  eqerlem  6137  erovlem  6198  dom2lem  6252  nneneq  6320  findcard2  6346  findcard2s  6347  ac6sfi  6352  indpi  6440  prarloclem3step  6594  prmuloc2  6665  ltexprlemm  6698  caucvgprprlemaddq  6806  caucvgsrlemgt1  6879  nn0ind-raph  8355  uzind4s  8533  indstr  8536  lbzbi  8551  fzrevral  8967  frecuzrdgfn  9198  climeu  9817  ch2varv  9908  elab1  9922  elab2a  9923  elabg2  9924  cbvrald  9927  bdsepnft  10007  bdsepnfALT  10009  bj-omssind  10059  bj-bdfindes  10074  bj-nn0suc0  10075  bj-nntrans  10076  bj-nnelirr  10078  bj-omtrans  10081  setindft  10090  bj-inf2vnlem3  10097  bj-inf2vnlem4  10098  bj-nn0sucALT  10103  bj-findis  10104  bj-findes  10106  strcollnft  10109  strcollnfALT  10111  sscoll2  10113