MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfim Unicode version

Theorem nfim 1920
Description: If is not free in and , it is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)
Hypotheses
Ref Expression
nfim.1
nfim.2
Assertion
Ref Expression
nfim

Proof of Theorem nfim
StepHypRef Expression
1 nfim.1 . 2
2 nfim.2 . . 3
32a1i 11 . 2
41, 3nfim1 1919 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  F/wnf 1616
This theorem is referenced by:  nfor  1935  nfnf  1949  nfia1  1954  cbval2  2027  mo2  2293  nfmo1  2295  mo3OLD  2324  moexex  2363  2eu4OLD  2381  2eu6OLD  2384  cbvralf  3078  vtocl2gf  3169  vtocl3gf  3170  vtoclgaf  3172  vtocl2gaf  3174  vtocl3gaf  3176  rspct  3203  rspc  3204  ralab2  3264  mob  3281  reu2eqd  3296  csbhypf  3453  cbvralcsf  3466  dfss2f  3494  rspn0  3797  elintab  4297  axrep2  4565  axrep3  4566  reusv2lem4  4656  reusv3  4660  nfpo  4810  nffr  4858  fv3  5884  tz6.12c  5890  fvmptss  5964  fvmptdf  5967  fvmptt  5971  fvmptf  5972  fmptco  6064  dff13f  6167  ovmpt2s  6426  ov2gf  6427  ovmpt2df  6434  ov3  6439  tfis  6689  tfinds  6694  tfindes  6697  findes  6730  dfoprab4f  6858  offval22  6879  tfr3  7087  dom2lem  7575  findcard2  7780  ac6sfi  7784  dfac8clem  8434  aceq1  8519  dfac5lem5  8529  zfcndrep  9013  zfcndinf  9017  pwfseqlem4a  9060  pwfseqlem4  9061  uzindOLD  10982  uzind4s  11170  rabssnn0fi  12095  seqof2  12165  rlim2  13319  ello1mpt  13344  o1compt  13410  summolem2a  13537  sumss  13546  o1fsum  13627  prodmolem2a  13741  fprodn0  13783  prmind2  14228  mreiincl  14993  gsumcom2  17003  gsummptnn0fz  17014  gsummoncoe1  18346  mdetralt2  19111  mdetunilem2  19115  bwthOLD  19911  ptcldmpt  20115  cnmptcom  20179  elmptrab  20328  isfildlem  20358  dvmptfsum  22376  dvfsumlem2  22428  dvfsumlem4  22430  dvfsumrlim  22432  dvfsum2  22435  coeeq2  22639  dgrle  22640  rlimcnp  23295  lgseisenlem2  23625  dchrisumlema  23673  dchrisumlem2  23675  dchrisumlem3  23676  mptelee  24198  isch3  26159  atom1d  27272  mo5f  27383  ssiun2sf  27427  ssrelf  27466  fmptcof2  27502  nn0min  27611  measiun  28189  lgamgulmlem2  28572  setinds  29210  tfisg  29284  wfisg  29289  frinsg  29325  ptrest  30048  subtr  30132  subtr2  30133  fdc1  30239  ac6s6  30580  fphpd  30750  monotuz  30877  monotoddzz  30879  oddcomabszz  30880  setindtrs  30967  aomclem6  31005  flcidc  31123  binomcxplemnotnn0  31261  fsumclf  31567  fsumsplitf  31568  fsummulc1f  31569  fsumnncl  31572  fsumsplit1  31573  fmul01  31574  fmuldfeqlem1  31576  fmuldfeq  31577  fmul01lt1lem1  31578  fmul01lt1lem2  31579  fproddivf  31588  fprodsplitf  31589  fprodsplit1f  31593  fprodexp  31600  fprodabs2  31602  climmulf  31610  climexp  31611  climsuse  31614  climrecf  31615  climinff  31617  climaddf  31621  mullimc  31622  idlimc  31632  neglimc  31653  addlimc  31654  0ellimcdiv  31655  limclner  31657  cncfshift  31676  cncfiooicclem1  31696  fprodcncf  31704  dvmptmulf  31734  dvnmptdivc  31735  dvnmul  31740  dvmptfprodlem  31741  dvmptfprod  31742  iblspltprt  31772  stoweidlem3  31785  stoweidlem26  31808  stoweidlem31  31813  stoweidlem34  31816  stoweidlem42  31824  stoweidlem43  31825  stoweidlem48  31830  stoweidlem51  31833  stoweidlem59  31841  fourierdlem86  31975  fourierdlem89  31978  fourierdlem91  31980  fourierdlem112  32001  2reu4a  32194  eu2ndop1stv  32207  2zrngmmgm  32752  bnj1385  33891  bnj1468  33904  bnj110  33916  bnj849  33983  bnj900  33987  bnj981  34008  bnj1014  34018  bnj1123  34042  bnj1128  34046  bnj1384  34088  bnj1489  34112  bnj1497  34116  bj-cbval2v  34302  bj-axrep2  34375  bj-axrep3  34376  fsumshftd  34682  fsumshftdOLD  34683  cdleme31sn1  36107  cdleme32fva  36163  cdlemk36  36639
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-12 1854
This theorem depends on definitions:  df-bi 185  df-ex 1613  df-nf 1617
  Copyright terms: Public domain W3C validator