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

Theorem nfv 1493
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 1491 . 2  |-  ( ph  ->  A. x ph )
21nfi 1423 1  |-  F/ x ph
Colors of variables: wff set class
Syntax hints:   F/wnf 1421
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 1410  ax-17 1491
This theorem depends on definitions:  df-bi 116  df-nf 1422
This theorem is referenced by:  nfvd  1494  alexim  1609  19.37aiv  1638  sbiedv  1747  spimv  1767  spimev  1817  19.36aiv  1857  cbval2  1873  cbvex2  1874  cbval2v  1875  cbvex2v  1876  cbvald  1877  cbvaldva  1880  cbvexdva  1881  eeanv  1884  sbco2h  1915  nfsbt  1927  sbnf2  1934  dfsb7a  1947  sbalyz  1952  sbco4lem  1959  sbco4  1960  dvelimALT  1963  eubidv  1985  sb8eu  1990  nfeudv  1992  nfeud  1993  nfeuv  1995  nfeu  1996  mobidv  2013  mo23  2018  sbmo  2036  mo4  2038  moimv  2043  moanimv  2052  bm1.1  2102  eqsb3lem  2220  eqsb3  2221  clelsb3  2222  clelsb4  2223  abbi  2231  abbidv  2235  cbvabv  2241  clelab  2242  nfcjust  2246  nfcv  2258  clelsb3f  2262  nfeqd  2273  nfeld  2274  nfabd  2277  dvelimdc  2278  cleqf  2282  sbabel  2284  ralbidva  2410  rexbidva  2411  ralbidv  2414  rexbidv  2415  2ralbida  2433  2ralbidva  2434  nfraldya  2446  nfrexdya  2447  rgen2a  2463  ralimdva  2476  ralrimiv  2481  r19.21v  2486  ralrimdv  2488  reximdvai  2509  r19.23v  2518  rexlimiv  2520  rexlimdv  2525  r19.29af  2550  r19.29an  2551  r19.29a  2552  r19.32vr  2556  r19.37av  2561  r19.41v  2564  reean  2576  reeanv  2577  reubidva  2590  rmobidva  2595  cbvralf  2625  cbvrexf  2626  cbvreu  2629  cbvralv  2631  cbvrexv  2632  cbvreuv  2633  cbvrmov  2634  cbvralsv  2642  cbvrexsv  2643  sbralie  2644  cbvrab  2658  cbvrabv  2659  issetf  2667  ceqsalv  2690  ceqsralv  2691  ceqsexv  2699  ceqsex2  2700  ceqsex2v  2701  vtocld  2712  vtocl  2714  vtocl2  2715  vtocl3  2716  vtoclg  2720  vtocl2g  2724  vtoclga  2726  vtocl2gaf  2727  vtocl2ga  2728  vtocl3gaf  2729  vtocl3ga  2730  spcimdv  2744  spcimedv  2746  spcgv  2747  spcegv  2748  rspct  2756  rspc  2757  rspce  2758  rspcv  2759  rspcev  2763  rspc2v  2776  eqvincg  2783  eqvincf  2784  ceqsexgv  2788  elabgt  2799  elab  2802  elabg  2803  elab3g  2808  elrab3t  2812  elrab  2813  ralab2  2821  rexab2  2823  eqeu  2827  mosubt  2834  mo2icl  2836  mob2  2837  mob  2839  reu2  2845  reu3  2847  rmo4f  2855  nfcdeq  2879  sbcco  2903  sbcco2  2904  cbvsbcv  2910  sbcieg  2913  sbcie2g  2914  sbcied  2917  elrabsf  2919  sbcbidv  2939  sbcg  2950  sbc2iegf  2951  sbc2ie  2952  rmo2ilem  2970  rmo3  2972  csbeq2dv  2998  nfcsb1d  3003  nfcsbd  3006  csbiebt  3009  csbied  3016  csbie2t  3018  sbcnestg  3023  sbnfc2  3030  cbvralcsf  3032  cbvrexcsf  3033  cbvreucsf  3034  cbvrabcsf  3035  cbvralv2  3036  cbvrexv2  3037  dfss2f  3058  uniiunlem  3155  abn0m  3358  rabn0m  3360  rabeq0  3362  abeq0  3363  r19.3rmv  3423  r19.28mv  3425  r19.27mv  3429  raaanv  3440  sbss  3441  nfifd  3469  euabsn  3563  oprcl  3699  nfuni  3712  nfunid  3713  eluniab  3718  nfint  3751  elintab  3752  iineq2dv  3805  disjiun  3894  opabbidv  3964  nfopab  3966  cbvopab  3969  cbvopabv  3970  cbvopab1  3971  cbvopab2  3972  cbvopab1s  3973  cbvopab1v  3974  mpteq12f  3978  mpteq2dva  3988  cbvmptf  3992  cbvmpt  3993  zfrep6  4015  zfnuleu  4022  intexabim  4047  iinexgm  4049  repizf2  4056  bnd  4066  copsex2t  4137  copsex2g  4138  opelopabsb  4152  opelopabaf  4165  pofun  4204  frind  4244  reusv3  4351  alxfr  4352  rexxfrd  4354  ralxfrALT  4358  onintonm  4403  sucprcreg  4434  eunex  4446  tfis  4467  tfis2  4469  tfisi  4471  peano2  4479  findes  4487  omsinds  4505  opeliunxp  4564  opeliunxp2  4649  ralxpf  4655  rexxpf  4656  dfdmf  4702  dfrnf  4750  elrnmpt1  4760  intirr  4895  nfiotadxy  5061  cbviota  5063  cbviotav  5064  sb8iota  5065  iota2d  5083  iota2  5084  dffun5r  5105  dffun6f  5106  dffun4f  5109  funco  5133  fun11  5160  imadif  5173  isarep1  5179  isarep2  5180  fun11iun  5356  fv3  5412  tz6.12f  5418  tz6.12c  5419  relelfvdm  5421  nfvres  5422  funimass4  5440  funfvdm2f  5454  fvmptss2  5464  fvmptdf  5476  fvmptdv  5477  fvmptt  5480  eqfnfv2f  5490  ralrnmpt  5530  rexrnmpt  5531  f1ompt  5539  ffnfv  5546  ffnfvf  5547  fmptco  5554  elabrex  5627  dff13f  5639  fliftfun  5665  cbvriota  5708  cbvriotav  5709  riota2  5720  riota5f  5722  acexmid  5741  nfoprab  5791  oprabbidv  5793  mpoeq123  5798  cbvoprab1  5811  cbvoprab2  5812  cbvoprab12  5813  cbvoprab12v  5814  cbvoprab3  5815  cbvoprab3v  5816  cbvmpox  5817  ralrnmpo  5853  ovmpodx  5865  ovmpodf  5870  ovmpodv  5871  ovi3  5875  ofrfval2  5966  abrexex2g  5986  opabex3d  5987  opabex3  5988  abrexex2  5990  dfoprab4f  6059  fmpox  6066  spc2ed  6098  cnvoprab  6099  f1od2  6100  opeliunxp2f  6103  tposoprab  6145  nfrecs  6172  tfri3  6232  nffrec  6261  eqerlem  6428  erovlem  6489  mptelixpg  6596  dom2lem  6634  xpf1o  6706  mapxpen  6710  nneneq  6719  findcard2  6751  findcard2s  6752  ac6sfi  6760  fiintim  6785  exmidomni  6982  fodjuomnilemdc  6984  ismkvnex  6997  mkvprop  7000  exmidfodomrlemr  7026  exmidfodomrlemrALT  7027  indpi  7118  prarloclem3step  7272  prmuloc2  7343  ltexprlemm  7376  caucvgprprlemaddq  7484  caucvgsrlemgt1  7571  suplocsrlem  7584  axpre-suploclemres  7677  nn0ind-raph  9126  uzind4s  9341  indstr  9344  supinfneg  9346  infsupneg  9347  lbzbi  9364  fzrevral  9840  frecuzrdgtcl  10140  frecuzrdgfunlem  10147  uzsinds  10170  seq3f1olemstep  10229  seq3f1olemp  10230  fimaxre2  10953  climeu  11020  nfsum1  11080  nfsum  11081  sumrbdclem  11100  summodclem2a  11105  zsumdc  11108  fsum3  11111  isumss  11115  isumss2  11117  fsum3cvg2  11118  fsumsplitf  11132  fsum2dlemstep  11158  fsum00  11186  fsumrelem  11195  mertenslem2  11260  divalglemeunn  11530  divalglemeuneg  11532  zsupcllemstep  11550  bezoutlemnewy  11596  bezoutlemmain  11598  bezoutlemzz  11602  bezout  11611  prmind2  11713  oddpwdclemdvds  11759  oddpwdclemndvds  11760  exmidunben  11850  ctiunctlemfo  11863  ctiunct  11864  cnmpt11  12363  cnmpt21  12371  cnmptcom  12378  imasnopn  12379  mulcncf  12671  ellimc3apf  12709  limccnp2cntop  12726  ch2varv  12871  elab1  12886  elab2a  12887  elabg2  12888  cbvrald  12891  sumdc2  12902  bdsepnft  12981  bdsepnfALT  12983  bj-omssind  13029  bj-bdfindes  13043  bj-nn0suc0  13044  bj-nntrans  13045  bj-nnelirr  13047  bj-omtrans  13050  setindft  13059  bj-inf2vnlem3  13066  bj-inf2vnlem4  13067  bj-nn0sucALT  13072  bj-findis  13073  bj-findes  13075  strcollnft  13078  strcollnfALT  13080  sscoll2  13082  isomninnlem  13121  trilpolemeq1  13129
  Copyright terms: Public domain W3C validator