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

Theorem nfv 1515
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 1513 . 2  |-  ( ph  ->  A. x ph )
21nfi 1449 1  |-  F/ x ph
Colors of variables: wff set class
Syntax hints:   F/wnf 1447
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 1436  ax-17 1513
This theorem depends on definitions:  df-bi 116  df-nf 1448
This theorem is referenced by:  nfvd  1516  alexim  1632  19.37aiv  1662  sbiedv  1776  spimv  1798  spimev  1848  19.36aiv  1888  cbval2  1908  cbvex2  1909  cbval2v  1910  cbvex2v  1911  cbvald  1912  cbvaldva  1915  cbvexdva  1916  eeanv  1919  nfsbv  1934  sbco2h  1951  nfsbt  1963  sbnf2  1968  dfsb7a  1981  sbalyz  1986  sbco4lem  1993  sbco4  1994  dvelimALT  1997  eubidv  2021  sb8eu  2026  nfeudv  2028  nfeud  2029  nfeuv  2031  nfeu  2032  mobidv  2049  mo23  2054  sbmo  2072  mo4  2074  moimv  2079  moanimv  2088  bm1.1  2149  eqsb3lem  2267  eqsb3  2268  clelsb3  2269  clelsb4  2270  abbi  2278  abbidv  2282  cbvabv  2289  clelab  2290  nfcjust  2294  nfcv  2306  clelsb3f  2310  nfeqd  2321  nfeld  2322  nfabdw  2325  nfabd  2326  dvelimdc  2327  cleqf  2331  sbabel  2333  ralbidva  2460  rexbidva  2461  ralbidv  2464  rexbidv  2465  2ralbida  2485  2ralbidva  2486  nfraldya  2499  nfrexdya  2500  rgen2a  2518  ralimdva  2531  ralrimiv  2536  r19.21v  2541  ralrimdv  2543  reximdvai  2564  r19.23v  2573  rexlimiv  2575  rexlimdv  2580  r19.29af  2605  r19.29an  2606  r19.29a  2607  r19.32vr  2612  r19.37av  2617  r19.41v  2620  reean  2632  reeanv  2633  reubidva  2646  rmobidva  2651  cbvralf  2683  cbvrexf  2684  cbvreu  2688  cbvralv  2690  cbvrexv  2691  cbvreuv  2692  cbvrmov  2693  cbvralsv  2704  cbvrexsv  2705  sbralie  2706  cbvrab  2720  cbvrabv  2721  issetf  2729  ceqsalv  2752  ceqsralv  2753  ceqsexv  2761  ceqsex2  2762  ceqsex2v  2763  vtocld  2774  vtocl  2776  vtocl2  2777  vtocl3  2778  vtoclg  2782  vtocl2g  2786  vtoclga  2788  vtocl2gaf  2789  vtocl2ga  2790  vtocl3gaf  2791  vtocl3ga  2792  spcimdv  2806  spcimedv  2808  spcgv  2809  spcegv  2810  rspct  2819  rspc  2820  rspce  2821  rspcv  2822  rspcev  2826  rspc2v  2839  eqvincg  2846  eqvincf  2847  ceqsexgv  2851  elabgt  2863  elab  2866  elabg  2868  elab3g  2873  elrab3t  2877  elrab  2878  ralab2  2886  rexab2  2888  eqeu  2892  mosubt  2899  mo2icl  2901  mob2  2902  mob  2904  reu2  2910  reu3  2912  rmo4f  2920  nfcdeq  2944  sbcco  2968  sbcco2  2969  cbvsbcv  2976  sbcieg  2979  sbcie2g  2980  sbcied  2983  elrabsf  2985  sbcbidv  3005  sbcg  3016  sbc2iegf  3017  sbc2ie  3018  rmo2ilem  3036  rmo3  3038  csbcow  3052  csbeq2dv  3067  nfcsb1d  3072  nfcsbd  3076  csbiebt  3080  csbied  3087  csbie2t  3089  sbcnestg  3094  sbnfc2  3101  cbvralcsf  3103  cbvrexcsf  3104  cbvreucsf  3105  cbvrabcsf  3106  cbvralv2  3107  cbvrexv2  3108  dfss2f  3129  uniiunlem  3227  abn0m  3430  rabn0m  3432  rabeq0  3434  abeq0  3435  r19.3rmv  3495  r19.28mv  3497  r19.27mv  3501  raaanv  3512  sbss  3513  nfifd  3543  euabsn  3641  oprcl  3777  nfuni  3790  nfunid  3791  eluniab  3796  nfint  3829  elintab  3830  iineq2dv  3883  disjiun  3972  opabbidv  4043  nfopab  4045  cbvopab  4048  cbvopabv  4049  cbvopab1  4050  cbvopab2  4051  cbvopab1s  4052  cbvopab1v  4053  mpteq12f  4057  mpteq2dva  4067  cbvmptf  4071  cbvmpt  4072  zfrep6  4094  zfnuleu  4101  intexabim  4126  iinexgm  4128  repizf2  4136  bnd  4146  copsex2t  4218  copsex2g  4219  opelopabsb  4233  opelopabaf  4246  pofun  4285  frind  4325  reusv3  4433  alxfr  4434  rexxfrd  4436  ralxfrALT  4440  onintonm  4489  sucprcreg  4521  eunex  4533  tfis  4555  tfis2  4557  tfisi  4559  peano2  4567  findes  4575  omsinds  4594  opeliunxp  4654  opeliunxp2  4739  ralxpf  4745  rexxpf  4746  dfdmf  4792  dfrnf  4840  elrnmpt1  4850  intirr  4985  nfiotadw  5151  cbviota  5153  cbviotav  5154  sb8iota  5155  iota2d  5173  iota2  5174  dffun5r  5195  dffun6f  5196  dffun4f  5199  funco  5223  fun11  5250  imadif  5263  isarep1  5269  isarep2  5270  fun11iun  5448  fv3  5504  tz6.12f  5510  tz6.12c  5511  relelfvdm  5513  nfvres  5514  funimass4  5532  funfvdm2f  5546  fvmptss2  5556  fvmptdf  5568  fvmptdv  5569  fvmptt  5572  eqfnfv2f  5582  ralrnmpt  5622  rexrnmpt  5623  f1ompt  5631  ffnfv  5638  ffnfvf  5639  fmptco  5646  elabrex  5721  dff13f  5733  fliftfun  5759  cbvriota  5803  cbvriotav  5804  riota2  5815  riota5f  5817  acexmid  5836  nfoprab  5886  oprabbidv  5888  mpoeq123  5893  cbvoprab1  5906  cbvoprab2  5907  cbvoprab12  5908  cbvoprab12v  5909  cbvoprab3  5910  cbvoprab3v  5911  cbvmpox  5912  ralrnmpo  5948  ovmpodx  5960  ovmpodf  5965  ovmpodv  5966  ovi3  5970  ofrfval2  6061  abrexex2g  6081  opabex3d  6082  opabex3  6083  abrexex2  6085  dfoprab4f  6154  fmpox  6161  spc2ed  6193  cnvoprab  6194  f1od2  6195  opeliunxp2f  6198  tposoprab  6240  nfrecs  6267  tfri3  6327  nffrec  6356  eqerlem  6524  erovlem  6585  mptelixpg  6692  dom2lem  6730  xpf1o  6802  mapxpen  6806  nneneq  6815  findcard2  6847  findcard2s  6848  ac6sfi  6856  fiintim  6886  exmidomni  7098  fodjuomnilemdc  7100  ismkvnex  7111  mkvprop  7114  exmidfodomrlemr  7150  exmidfodomrlemrALT  7151  cc3  7201  indpi  7275  prarloclem3step  7429  prmuloc2  7500  ltexprlemm  7533  caucvgprprlemaddq  7641  caucvgsrlemgt1  7728  suplocsrlem  7741  axpre-suploclemres  7834  nn0ind-raph  9300  uzind4s  9520  indstr  9523  supinfneg  9525  infsupneg  9526  lbzbi  9546  fzrevral  10031  frecuzrdgtcl  10338  frecuzrdgfunlem  10345  uzsinds  10368  seq3f1olemstep  10427  seq3f1olemp  10428  fimaxre2  11158  climeu  11227  nfsum1  11287  nfsum  11288  sumrbdclem  11308  summodclem2a  11312  zsumdc  11315  fsum3  11318  isumss  11322  isumss2  11324  fsum3cvg2  11325  fsumsplitf  11339  fsum2dlemstep  11365  fsum00  11393  fsumrelem  11402  mertenslem2  11467  nfcprod1  11485  nfcprod  11486  prodeq2  11488  prodrbdclem  11502  prodmodclem2a  11507  zproddc  11510  fprodseq  11514  fprodntrivap  11515  prodssdc  11520  fprodcl2lem  11536  fprod2dlemstep  11553  fprodsplitf  11563  fprodsplit1f  11565  fprodap0f  11567  fprodle  11571  divalglemeunn  11847  divalglemeuneg  11849  zsupcllemstep  11867  bezoutlemnewy  11918  bezoutlemmain  11920  bezoutlemzz  11924  bezout  11933  nnwofdc  11960  prmind2  12041  oddpwdclemdvds  12091  oddpwdclemndvds  12092  pcmpt  12262  pcmptdvds  12264  exmidunben  12322  ctiunctlemfo  12335  ctiunct  12336  ctiunctal  12337  cnmpt11  12850  cnmpt21  12858  cnmptcom  12865  imasnopn  12866  mulcncf  13158  ellimc3apf  13196  limccnp2cntop  13213  ch2varv  13511  elab1  13526  elab2a  13527  elabg2  13528  cbvrald  13531  sumdc2  13542  bdsepnft  13631  bdsepnfALT  13633  bj-omssind  13679  bj-bdfindes  13693  bj-nn0suc0  13694  bj-nntrans  13695  bj-nnelirr  13697  bj-omtrans  13700  setindft  13709  bj-inf2vnlem3  13716  bj-inf2vnlem4  13717  bj-nn0sucALT  13722  bj-findis  13723  bj-findes  13725  strcollnft  13728  strcollnfALT  13730  pw1nct  13745  isomninnlem  13771  trilpolemeq1  13781  trirec0  13785  iswomninnlem  13790  ismkvnnlem  13793  nconstwlpolemgt0  13804
  Copyright terms: Public domain W3C validator