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

Theorem nfv 1437
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 1435 . 2  |-  ( ph  ->  A. x ph )
21nfi 1367 1  |-  F/ x ph
Colors of variables: wff set class
Syntax hints:   F/wnf 1365
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-gen 1354  ax-17 1435
This theorem depends on definitions:  df-bi 114  df-nf 1366
This theorem is referenced by:  nfvd  1438  alexim  1552  19.37aiv  1581  sbiedv  1688  spimv  1708  spimev  1757  19.36aiv  1797  cbval2  1812  cbvex2  1813  cbval2v  1814  cbvex2v  1815  cbvald  1816  cbvaldva  1819  cbvexdva  1820  eeanv  1823  sbco2h  1854  nfsbt  1866  sbnf2  1873  dfsb7a  1886  sbalyz  1891  sbco4lem  1898  sbco4  1899  dvelimALT  1902  eubidv  1924  sb8eu  1929  nfeudv  1931  nfeud  1932  nfeuv  1934  nfeu  1935  mobidv  1952  mo23  1957  sbmo  1975  mo4  1977  moimv  1982  moanimv  1991  bm1.1  2041  eqsb3lem  2156  eqsb3  2157  clelsb3  2158  clelsb4  2159  abbi  2167  abbidv  2171  cbvabv  2177  clelab  2178  nfcjust  2182  nfcv  2194  nfeqd  2208  nfeld  2209  nfabd  2212  dvelimdc  2213  cleqf  2217  sbabel  2219  ralbidva  2339  rexbidva  2340  ralbidv  2343  rexbidv  2344  2ralbida  2362  2ralbidva  2363  nfraldya  2375  nfrexdya  2376  rgen2a  2392  ralimdva  2404  ralrimiv  2408  r19.21v  2413  ralrimdv  2415  reximdvai  2436  r19.23v  2442  rexlimiv  2444  rexlimdv  2449  r19.29af  2470  r19.29a  2471  r19.32vr  2475  r19.37av  2480  r19.41v  2483  reean  2495  reeanv  2496  reubidva  2509  rmobidva  2514  cbvralf  2544  cbvrexf  2545  cbvreu  2548  cbvralv  2550  cbvrexv  2551  cbvreuv  2552  cbvrmov  2553  cbvralsv  2561  cbvrexsv  2562  sbralie  2563  cbvrab  2572  cbvrabv  2573  issetf  2579  ceqsalv  2601  ceqsralv  2602  ceqsexv  2610  ceqsex2  2611  ceqsex2v  2612  vtocld  2623  vtocl  2625  vtocl2  2626  vtocl3  2627  vtoclg  2630  vtocl2g  2634  vtoclga  2636  vtocl2gaf  2637  vtocl2ga  2638  vtocl3gaf  2639  vtocl3ga  2640  spcimdv  2654  spcimedv  2656  spcgv  2657  spcegv  2658  rspct  2666  rspc  2667  rspce  2668  rspcv  2669  rspcev  2673  rspc2v  2685  eqvincg  2691  eqvincf  2692  ceqsexgv  2696  elabgt  2707  elab  2710  elabg  2711  elab3g  2716  elrab3t  2720  elrab  2721  ralab2  2728  rexab2  2730  eqeu  2734  mosubt  2741  mo2icl  2743  mob2  2744  mob  2746  reu2  2752  reu3  2754  nfcdeq  2784  sbcco  2808  sbcco2  2809  cbvsbcv  2815  sbcieg  2818  sbcie2g  2819  sbcied  2822  elrabsf  2824  sbcbidv  2844  sbcg  2855  sbc2iegf  2856  sbc2ie  2857  rmo2ilem  2875  rmo3  2877  csbeq2dv  2903  nfcsb1d  2908  nfcsbd  2911  csbiebt  2914  csbied  2920  csbie2t  2922  sbcnestg  2927  sbnfc2  2934  cbvralcsf  2936  cbvrexcsf  2937  cbvreucsf  2938  cbvrabcsf  2939  cbvralv2  2940  cbvrexv2  2941  dfss2f  2964  uniiunlem  3056  rabn0m  3273  rabeq0  3275  abeq0  3276  r19.3rmv  3340  r19.28mv  3342  r19.27mv  3345  raaanv  3356  sbss  3357  nfifd  3383  euabsn  3468  oprcl  3601  nfuni  3614  nfunid  3615  eluniab  3620  nfint  3653  elintab  3654  iineq2dv  3707  opabbidv  3851  nfopab  3853  cbvopab  3856  cbvopabv  3857  cbvopab1  3858  cbvopab2  3859  cbvopab1s  3860  cbvopab1v  3861  mpteq12f  3865  mpteq2dva  3875  cbvmpt  3879  zfrep6  3902  zfnuleu  3909  intexabim  3934  iinexgm  3936  repizf2  3943  bnd  3953  copsex2t  4010  copsex2g  4011  opelopabsb  4025  opelopabaf  4038  pofun  4077  frind  4117  reusv3  4220  alxfr  4221  rexxfrd  4223  ralxfrALT  4227  onintonm  4271  sucprcreg  4301  eunex  4313  tfis  4334  tfis2  4336  tfisi  4338  peano2  4346  findes  4354  opeliunxp  4423  opeliunxp2  4504  ralxpf  4510  rexxpf  4511  dfdmf  4556  dfrnf  4603  elrnmpt1  4613  intirr  4739  nfiotadxy  4898  cbviota  4900  cbviotav  4901  sb8iota  4902  iota2d  4920  iota2  4921  dffun5r  4942  dffun6f  4943  dffun4f  4946  funco  4968  fun11  4994  imadif  5007  isarep1  5013  isarep2  5014  fun11iun  5175  fv3  5225  tz6.12f  5230  tz6.12c  5231  relelfvdm  5233  nfvres  5234  funimass4  5252  funfvdm2f  5266  fvmptss2  5275  fvmptdf  5286  fvmptdv  5287  fvmptt  5290  eqfnfv2f  5297  ralrnmpt  5337  rexrnmpt  5338  f1ompt  5348  ffnfv  5351  ffnfvf  5352  fmptco  5358  elabrex  5425  dff13f  5437  fliftfun  5464  cbvriota  5506  cbvriotav  5507  riota2  5518  riota5f  5520  acexmid  5539  nfoprab  5585  oprabbidv  5587  mpt2eq123  5592  cbvoprab1  5604  cbvoprab2  5605  cbvoprab12  5606  cbvoprab12v  5607  cbvoprab3  5608  cbvoprab3v  5609  cbvmpt2x  5610  ralrnmpt2  5643  ovmpt2dx  5655  ovmpt2df  5660  ovmpt2dv  5661  ovi3  5665  ofrfval2  5755  abrexex2g  5775  opabex3d  5776  opabex3  5777  abrexex2  5779  dfoprab4f  5847  fmpt2x  5854  spc2ed  5882  cnvoprab  5883  f1od2  5884  tposoprab  5926  nfrecs  5953  tfri3  5984  nffrec  6013  eqerlem  6168  erovlem  6229  dom2lem  6283  nneneq  6351  findcard2  6377  findcard2s  6378  ac6sfi  6383  indpi  6498  prarloclem3step  6652  prmuloc2  6723  ltexprlemm  6756  caucvgprprlemaddq  6864  caucvgsrlemgt1  6937  nn0ind-raph  8414  uzind4s  8629  indstr  8632  lbzbi  8648  fzrevral  9069  frecuzrdgfn  9362  climeu  10048  divalglemeunn  10233  divalglemeuneg  10235  oddpwdclemdvds  10258  oddpwdclemndvds  10259  ch2varv  10295  elab1  10309  elab2a  10310  elabg2  10311  cbvrald  10314  bdsepnft  10394  bdsepnfALT  10396  bj-omssind  10446  bj-bdfindes  10461  bj-nn0suc0  10462  bj-nntrans  10463  bj-nnelirr  10465  bj-omtrans  10468  setindft  10477  bj-inf2vnlem3  10484  bj-inf2vnlem4  10485  bj-nn0sucALT  10490  bj-findis  10491  bj-findes  10493  strcollnft  10496  strcollnfALT  10498  sscoll2  10500
  Copyright terms: Public domain W3C validator