ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nfv GIF version

Theorem nfv 1464
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
StepHypRef Expression
1 ax-17 1462 . 2 (𝜑 → ∀𝑥𝜑)
21nfi 1394 1 𝑥𝜑
Colors of variables: wff set class
Syntax hints:  wnf 1392
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-gen 1381  ax-17 1462
This theorem depends on definitions:  df-bi 115  df-nf 1393
This theorem is referenced by:  nfvd  1465  alexim  1579  19.37aiv  1608  sbiedv  1716  spimv  1736  spimev  1786  19.36aiv  1826  cbval2  1841  cbvex2  1842  cbval2v  1843  cbvex2v  1844  cbvald  1845  cbvaldva  1848  cbvexdva  1849  eeanv  1852  sbco2h  1883  nfsbt  1895  sbnf2  1902  dfsb7a  1915  sbalyz  1920  sbco4lem  1927  sbco4  1928  dvelimALT  1931  eubidv  1953  sb8eu  1958  nfeudv  1960  nfeud  1961  nfeuv  1963  nfeu  1964  mobidv  1981  mo23  1986  sbmo  2004  mo4  2006  moimv  2011  moanimv  2020  bm1.1  2070  eqsb3lem  2187  eqsb3  2188  clelsb3  2189  clelsb4  2190  abbi  2198  abbidv  2202  cbvabv  2208  clelab  2209  nfcjust  2213  nfcv  2225  nfeqd  2239  nfeld  2240  nfabd  2243  dvelimdc  2244  cleqf  2248  sbabel  2250  ralbidva  2372  rexbidva  2373  ralbidv  2376  rexbidv  2377  2ralbida  2395  2ralbidva  2396  nfraldya  2408  nfrexdya  2409  rgen2a  2425  ralimdva  2437  ralrimiv  2441  r19.21v  2446  ralrimdv  2448  reximdvai  2469  r19.23v  2477  rexlimiv  2479  rexlimdv  2484  r19.29af  2505  r19.29an  2506  r19.29a  2507  r19.32vr  2511  r19.37av  2516  r19.41v  2519  reean  2531  reeanv  2532  reubidva  2545  rmobidva  2550  cbvralf  2580  cbvrexf  2581  cbvreu  2584  cbvralv  2586  cbvrexv  2587  cbvreuv  2588  cbvrmov  2589  cbvralsv  2597  cbvrexsv  2598  sbralie  2599  cbvrab  2613  cbvrabv  2614  issetf  2620  ceqsalv  2643  ceqsralv  2644  ceqsexv  2652  ceqsex2  2653  ceqsex2v  2654  vtocld  2665  vtocl  2667  vtocl2  2668  vtocl3  2669  vtoclg  2672  vtocl2g  2676  vtoclga  2678  vtocl2gaf  2679  vtocl2ga  2680  vtocl3gaf  2681  vtocl3ga  2682  spcimdv  2696  spcimedv  2698  spcgv  2699  spcegv  2700  rspct  2708  rspc  2709  rspce  2710  rspcv  2711  rspcev  2715  rspc2v  2726  eqvincg  2732  eqvincf  2733  ceqsexgv  2737  elabgt  2748  elab  2751  elabg  2752  elab3g  2757  elrab3t  2761  elrab  2762  ralab2  2770  rexab2  2772  eqeu  2776  mosubt  2783  mo2icl  2785  mob2  2786  mob  2788  reu2  2794  reu3  2796  nfcdeq  2826  sbcco  2850  sbcco2  2851  cbvsbcv  2857  sbcieg  2860  sbcie2g  2861  sbcied  2864  elrabsf  2866  sbcbidv  2886  sbcg  2897  sbc2iegf  2898  sbc2ie  2899  rmo2ilem  2917  rmo3  2919  csbeq2dv  2945  nfcsb1d  2950  nfcsbd  2953  csbiebt  2956  csbied  2963  csbie2t  2965  sbcnestg  2970  sbnfc2  2977  cbvralcsf  2979  cbvrexcsf  2980  cbvreucsf  2981  cbvrabcsf  2982  cbvralv2  2983  cbvrexv2  2984  dfss2f  3005  uniiunlem  3098  abn0m  3297  rabn0m  3299  rabeq0  3301  abeq0  3302  r19.3rmv  3359  r19.28mv  3361  r19.27mv  3365  raaanv  3376  sbss  3377  nfifd  3404  euabsn  3495  oprcl  3629  nfuni  3642  nfunid  3643  eluniab  3648  nfint  3681  elintab  3682  iineq2dv  3735  opabbidv  3879  nfopab  3881  cbvopab  3884  cbvopabv  3885  cbvopab1  3886  cbvopab2  3887  cbvopab1s  3888  cbvopab1v  3889  mpteq12f  3893  mpteq2dva  3903  cbvmptf  3907  cbvmpt  3908  zfrep6  3931  zfnuleu  3938  intexabim  3963  iinexgm  3965  repizf2  3972  bnd  3982  copsex2t  4046  copsex2g  4047  opelopabsb  4061  opelopabaf  4074  pofun  4113  frind  4153  reusv3  4256  alxfr  4257  rexxfrd  4259  ralxfrALT  4263  onintonm  4307  sucprcreg  4338  eunex  4350  tfis  4371  tfis2  4373  tfisi  4375  peano2  4383  findes  4391  omsinds  4408  opeliunxp  4461  opeliunxp2  4544  ralxpf  4550  rexxpf  4551  dfdmf  4597  dfrnf  4644  elrnmpt1  4654  intirr  4785  nfiotadxy  4949  cbviota  4951  cbviotav  4952  sb8iota  4953  iota2d  4971  iota2  4972  dffun5r  4993  dffun6f  4994  dffun4f  4997  funco  5019  fun11  5046  imadif  5059  isarep1  5065  isarep2  5066  fun11iun  5237  fv3  5291  tz6.12f  5296  tz6.12c  5297  relelfvdm  5299  nfvres  5300  funimass4  5318  funfvdm2f  5332  fvmptss2  5342  fvmptdf  5353  fvmptdv  5354  fvmptt  5357  eqfnfv2f  5364  ralrnmpt  5404  rexrnmpt  5405  f1ompt  5413  ffnfv  5419  ffnfvf  5420  fmptco  5427  elabrex  5498  dff13f  5510  fliftfun  5536  cbvriota  5579  cbvriotav  5580  riota2  5591  riota5f  5593  acexmid  5612  nfoprab  5658  oprabbidv  5660  mpt2eq123  5665  cbvoprab1  5677  cbvoprab2  5678  cbvoprab12  5679  cbvoprab12v  5680  cbvoprab3  5681  cbvoprab3v  5682  cbvmpt2x  5683  ralrnmpt2  5716  ovmpt2dx  5728  ovmpt2df  5733  ovmpt2dv  5734  ovi3  5738  ofrfval2  5828  abrexex2g  5848  opabex3d  5849  opabex3  5850  abrexex2  5852  dfoprab4f  5920  fmpt2x  5927  spc2ed  5955  cnvoprab  5956  f1od2  5957  tposoprab  5999  nfrecs  6026  tfri3  6086  nffrec  6115  eqerlem  6275  erovlem  6336  dom2lem  6441  xpf1o  6512  mapxpen  6516  nneneq  6525  findcard2  6557  findcard2s  6558  ac6sfi  6566  exmidomni  6742  fodjuomnilemdc  6743  exmidfodomrlemr  6772  exmidfodomrlemrALT  6773  indpi  6845  prarloclem3step  6999  prmuloc2  7070  ltexprlemm  7103  caucvgprprlemaddq  7211  caucvgsrlemgt1  7284  nn0ind-raph  8796  uzind4s  9010  indstr  9013  supinfneg  9015  infsupneg  9016  lbzbi  9033  fzrevral  9449  frecuzrdgtcl  9747  frecuzrdgfunlem  9754  uzsinds  9776  iseqf1olemstep  9834  iseqf1olemp  9835  fimaxre2  10551  climeu  10577  nfsum1  10635  nfsum  10636  isumrblem  10655  isummolem2a  10660  zisum  10663  fisum  10665  isumss  10669  divalglemeunn  10796  divalglemeuneg  10798  zsupcllemstep  10816  bezoutlemnewy  10860  bezoutlemmain  10862  bezoutlemzz  10866  bezout  10875  prmind2  10977  oddpwdclemdvds  11023  oddpwdclemndvds  11024  ch2varv  11107  elab1  11121  elab2a  11122  elabg2  11123  cbvrald  11126  sumdc2  11137  bdsepnft  11216  bdsepnfALT  11218  bj-omssind  11268  bj-bdfindes  11282  bj-nn0suc0  11283  bj-nntrans  11284  bj-nnelirr  11286  bj-omtrans  11289  setindft  11298  bj-inf2vnlem3  11305  bj-inf2vnlem4  11306  bj-nn0sucALT  11311  bj-findis  11312  bj-findes  11314  strcollnft  11317  strcollnfALT  11319  sscoll2  11321
  Copyright terms: Public domain W3C validator