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

Theorem nfv 1464
Description: If  x is not present in  ph, then  x is not free in  ph. (Contributed by Mario Carneiro, 11-Aug-2016.)
Assertion
Ref Expression
nfv  |-  F/ x ph
Distinct variable group:    ph, x

Proof of Theorem nfv
StepHypRef Expression
1 ax-17 1462 . 2  |-  ( ph  ->  A. x ph )
21nfi 1394 1  |-  F/ x ph
Colors of variables: wff set class
Syntax hints:   F/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  3497  oprcl  3631  nfuni  3644  nfunid  3645  eluniab  3650  nfint  3683  elintab  3684  iineq2dv  3737  opabbidv  3881  nfopab  3883  cbvopab  3886  cbvopabv  3887  cbvopab1  3888  cbvopab2  3889  cbvopab1s  3890  cbvopab1v  3891  mpteq12f  3895  mpteq2dva  3905  cbvmptf  3909  cbvmpt  3910  zfrep6  3933  zfnuleu  3940  intexabim  3965  iinexgm  3967  repizf2  3974  bnd  3984  copsex2t  4048  copsex2g  4049  opelopabsb  4063  opelopabaf  4076  pofun  4115  frind  4155  reusv3  4258  alxfr  4259  rexxfrd  4261  ralxfrALT  4265  onintonm  4309  sucprcreg  4340  eunex  4352  tfis  4373  tfis2  4375  tfisi  4377  peano2  4385  findes  4393  omsinds  4410  opeliunxp  4463  opeliunxp2  4546  ralxpf  4552  rexxpf  4553  dfdmf  4599  dfrnf  4646  elrnmpt1  4656  intirr  4787  nfiotadxy  4951  cbviota  4953  cbviotav  4954  sb8iota  4955  iota2d  4973  iota2  4974  dffun5r  4995  dffun6f  4996  dffun4f  4999  funco  5021  fun11  5048  imadif  5061  isarep1  5067  isarep2  5068  fun11iun  5239  fv3  5293  tz6.12f  5298  tz6.12c  5299  relelfvdm  5301  nfvres  5302  funimass4  5320  funfvdm2f  5334  fvmptss2  5344  fvmptdf  5355  fvmptdv  5356  fvmptt  5359  eqfnfv2f  5366  ralrnmpt  5406  rexrnmpt  5407  f1ompt  5415  ffnfv  5421  ffnfvf  5422  fmptco  5429  elabrex  5500  dff13f  5512  fliftfun  5538  cbvriota  5581  cbvriotav  5582  riota2  5593  riota5f  5595  acexmid  5614  nfoprab  5660  oprabbidv  5662  mpt2eq123  5667  cbvoprab1  5679  cbvoprab2  5680  cbvoprab12  5681  cbvoprab12v  5682  cbvoprab3  5683  cbvoprab3v  5684  cbvmpt2x  5685  ralrnmpt2  5718  ovmpt2dx  5730  ovmpt2df  5735  ovmpt2dv  5736  ovi3  5740  ofrfval2  5830  abrexex2g  5850  opabex3d  5851  opabex3  5852  abrexex2  5854  dfoprab4f  5922  fmpt2x  5929  spc2ed  5957  cnvoprab  5958  f1od2  5959  tposoprab  6001  nfrecs  6028  tfri3  6088  nffrec  6117  eqerlem  6277  erovlem  6338  dom2lem  6443  xpf1o  6514  mapxpen  6518  nneneq  6527  findcard2  6559  findcard2s  6560  ac6sfi  6568  exmidomni  6745  fodjuomnilemdc  6746  exmidfodomrlemr  6775  exmidfodomrlemrALT  6776  indpi  6848  prarloclem3step  7002  prmuloc2  7073  ltexprlemm  7106  caucvgprprlemaddq  7214  caucvgsrlemgt1  7287  nn0ind-raph  8799  uzind4s  9013  indstr  9016  supinfneg  9018  infsupneg  9019  lbzbi  9036  fzrevral  9452  frecuzrdgtcl  9750  frecuzrdgfunlem  9757  uzsinds  9779  iseqf1olemstep  9838  iseqf1olemp  9839  fimaxre2  10556  climeu  10582  nfsum1  10640  nfsum  10641  isumrblem  10660  isummolem2a  10665  zisum  10668  fisum  10670  isumss  10674  isumss2  10676  fisumcvg2  10677  fsumsplitf  10690  divalglemeunn  10827  divalglemeuneg  10829  zsupcllemstep  10847  bezoutlemnewy  10891  bezoutlemmain  10893  bezoutlemzz  10897  bezout  10906  prmind2  11008  oddpwdclemdvds  11054  oddpwdclemndvds  11055  ch2varv  11138  elab1  11152  elab2a  11153  elabg2  11154  cbvrald  11157  sumdc2  11168  bdsepnft  11247  bdsepnfALT  11249  bj-omssind  11299  bj-bdfindes  11313  bj-nn0suc0  11314  bj-nntrans  11315  bj-nnelirr  11317  bj-omtrans  11320  setindft  11329  bj-inf2vnlem3  11336  bj-inf2vnlem4  11337  bj-nn0sucALT  11342  bj-findis  11343  bj-findes  11345  strcollnft  11348  strcollnfALT  11350  sscoll2  11352
  Copyright terms: Public domain W3C validator