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

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

Proof of Theorem nfan
StepHypRef Expression
1 nfan.1 . 2
2 nfan.2 . . 3
32a1i 11 . 2
41, 3nfan1 1927 1
Colors of variables: wff setvar class
Syntax hints:  /\wa 369  F/wnf 1616
This theorem is referenced by:  nfnan  1929  nf3an  1930  hban  1931  cbvex2OLD  2029  nfeqf  2045  nfald2  2073  nfsb4t  2130  2ax6elem  2193  eupicka  2359  mopick2  2362  2mo  2373  2moOLD  2374  2eu6OLD  2384  axbnd  2434  clelab  2601  clelabOLD  2602  nfelOLD  2633  nfabd2  2640  2ralbida  2898  r19.29an  2998  ralcom2  3022  reean  3024  cbvreu  3082  cbvrab  3107  ceqsex2  3147  vtocl2gaf  3174  rspce  3205  eqvincf  3227  elrabf  3255  elrab3t  3256  rexab2  3266  morex  3283  reu2  3287  reu2eqd  3296  sbc2iegf  3402  rmo2  3427  rmo3  3429  csbiebt  3454  csbie2t  3463  cbvreucsf  3468  cbvrabcsf  3469  rabsnifsb  4098  nfop  4233  nfopd  4234  eluniab  4260  dfnfc2  4267  rabasiun  4334  nfopab  4517  cbvopab  4520  cbvopab1  4522  cbvopab2  4523  cbvopab1s  4524  mpteq12f  4528  nfmpt  4540  cbvmpt  4542  axrep3  4566  axrep4  4567  axrep5  4568  reusv2lem2  4654  reusv2lem3  4655  reusv6OLD  4663  nfpo  4810  nfso  4811  nffr  4858  nfwe  4860  nfxp  5031  opeliunxp  5056  nfco  5173  elrnmpt1  5256  nfimad  5351  iota2  5582  nffun  5615  imadif  5668  nffn  5682  nff  5732  nff1  5784  nffo  5799  nff1o  5819  nffvd  5880  fv3  5884  fmptco  6064  nfiso  6220  nfriotad  6265  cbvriota  6267  riota2df  6278  riota5f  6282  oprabv  6345  nfoprab  6349  mpt2eq123  6356  nfmpt2  6366  cbvoprab1  6369  cbvoprab2  6370  cbvoprab12  6371  cbvoprab3  6373  cbvmpt2x  6375  ovmpt2dxf  6428  elovmpt2rab  6521  elovmpt2rab1  6522  onminex  6642  peano5  6723  fun11iun  6760  opabex3d  6778  opabex3  6779  dfoprab4f  6858  fmpt2x  6866  nfrecs  7063  tfr3  7087  tz7.49  7129  erovlem  7426  nfixp  7508  nfixp1  7509  xpf1o  7699  nneneq  7720  ac6sfi  7784  nfoi  7960  wdom2d  8027  infpssrlem4  8707  hsmexlem2  8828  hsmexlem4  8830  domtriomlem  8843  axdc3lem2  8852  axdc4lem  8856  zorn2lem4  8900  zorn2lem5  8901  konigthlem  8964  axextnd  8987  axrepndlem2  8989  axrepnd  8990  axunnd  8992  axpowndlem2  8994  axpowndlem2OLD  8995  axpowndlem4  8998  axpownd  8999  axregndlem2  9001  axregnd  9002  axregndOLD  9003  axinfndlem1  9004  axinfnd  9005  zfcndrep  9013  zfcndinf  9017  dedekind  9765  dedekindle  9766  fsuppmapnn0fiublem  12096  fsuppmapnn0fiub  12097  fsuppmapnn0fiubex  12098  nfsum1  13512  nfsum  13513  fsum2dlem  13585  fsum00  13612  nfcprod1  13717  nfcprod  13718  fprod2dlem  13784  mreexexd  15045  acsmapd  15808  gsum2d2lem  17001  dprd2d2  17093  gsummoncoe1  18346  gsummatr01lem4  19160  cpmatmcllem  19219  pmatcollpwfi  19283  cayleyhamilton1  19393  neiptopnei  19633  neiptopreu  19634  neitr  19681  iunconlem  19928  iuncon  19929  ptcnplem  20122  ptcnp  20123  xkocnv  20315  isfildlem  20358  utopsnneiplem  20750  isucn2  20782  cfilucfilOLD  21072  cfilucfil  21073  restmetu  21090  ovolfiniun  21912  ovoliunlem3  21915  ovoliunnul  21918  volfiniun  21957  itg2splitlem  22155  itg2split  22156  isibl2  22173  nfitg  22181  cbvitg  22182  limciun  22298  istrkg2ld  23858  chirred  27314  spc2ed  27372  mo5f  27383  rmo3f  27394  rmo4fOLD  27395  foresf1o  27403  cbvdisjf  27434  disjabrex  27443  disjabrexf  27444  funimass4f  27474  cbvmptf  27494  fmptcof2  27502  fcomptf  27503  funcnv4mpt  27512  cnvoprab  27546  f1od2  27547  fpwrelmap  27556  xrofsup  27582  nn0min  27611  2sqmo  27637  isarchiofld  27807  reff  27842  locfinreflem  27843  cmpcref  27853  ordtconlem1  27906  esumcl  28043  gsumesum  28067  esumlub  28068  esumcst  28071  esumfzf  28075  esumfsup  28076  hasheuni  28091  esumcvg  28092  measvunilem  28183  measvunilem0  28184  measvuni  28185  measinblem  28191  voliune  28201  volfiniune  28202  volmeas  28203  oms0  28266  eulerpartlemgvv  28315  dstrvprob  28410  cvmcov  28708  iota5f  29102  axextdist  29232  axext4dist  29233  trpredmintr  29314  nfwrecs  29338  wfrlem4  29346  nfwlim  29378  frrlem4  29390  wl-cbvalnaed  29985  wl-2sb6d  30008  wl-sbalnae  30012  wl-ax11-lem3  30027  heicant  30049  mbfposadd  30062  ftc1anclem5  30094  finminlem  30136  indexdom  30225  filbcmb  30231  sdclem2  30235  sdclem1  30236  fdc1  30239  mzpsubmpt  30675  mzpexpmpt  30677  eq0rabdioph  30710  eqrabdioph  30711  setindtr  30966  binomcxplemnotnn0  31261  elunif  31391  rspcegf  31398  fnchoice  31404  refsumcn  31405  rfcnnnub  31411  upbdrech  31505  ssfiunibd  31509  iccshift  31558  iooshift  31562  fsumclf  31567  fsumsplitf  31568  fsummulc1f  31569  fsumsplit1  31573  fmul01  31574  fmuldfeqlem1  31576  fmuldfeq  31577  fmul01lt1lem1  31578  fmul01lt1lem2  31579  infrglb  31584  fprodsplitf  31589  fprodsplit1f  31593  fprodexp  31600  fprodle  31604  mccl  31606  climmulf  31610  climexp  31611  climsuse  31614  climrecf  31615  climinff  31617  climaddf  31621  mullimc  31622  islptre  31625  climf  31628  mullimcf  31629  rexlim2d  31631  idlimc  31632  limcperiod  31634  limcrecl  31635  islpcn  31645  limsupre  31647  limcleqr  31650  addlimc  31654  limclner  31657  cncficcgt0  31691  cncfioobd  31700  dvmptmulf  31734  dvnmul  31740  dvmptfprodlem  31741  dvmptfprod  31742  dvnprodlem1  31743  dvnprodlem2  31744  iblsplitf  31769  itgperiod  31780  stoweidlem3  31785  stoweidlem26  31808  stoweidlem27  31809  stoweidlem29  31811  stoweidlem31  31813  stoweidlem34  31816  stoweidlem35  31817  stoweidlem36  31818  stoweidlem39  31821  stoweidlem42  31824  stoweidlem43  31825  stoweidlem44  31826  stoweidlem46  31828  stoweidlem48  31830  stoweidlem49  31831  stoweidlem51  31833  stoweidlem52  31834  stoweidlem53  31835  stoweidlem54  31836  stoweidlem55  31837  stoweidlem56  31838  stoweidlem57  31839  stoweidlem58  31840  stoweidlem59  31841  stoweidlem60  31842  stoweidlem61  31843  stoweidlem62  31844  stoweid  31845  wallispilem3  31849  stirlinglem13  31868  stirling  31871  fourierdlem16  31905  fourierdlem21  31910  fourierdlem22  31911  fourierdlem31  31920  fourierdlem39  31928  fourierdlem48  31937  fourierdlem51  31940  fourierdlem53  31942  fourierdlem68  31957  fourierdlem71  31960  fourierdlem73  31962  fourierdlem80  31969  fourierdlem81  31970  fourierdlem86  31975  fourierdlem87  31976  fourierdlem93  31982  fourierdlem94  31983  fourierdlem103  31992  fourierdlem104  31993  fourierdlem112  32001  fourierdlem113  32002  elaa2  32017  etransclem32  32049  nfdfat  32215  2zrngmmgm  32752  opeliun2xp  32922  cbvmpt2x2  32925  ovmpt2rdxf  32928  aacllem  33216  iunconlem2  33735  bnj919  33825  bnj1146  33850  bnj1379  33889  bnj849  33983  bnj916  33991  bnj964  34001  bnj1014  34018  bnj1123  34042  bnj1228  34067  bnj1307  34079  bnj1321  34083  bnj1398  34090  bnj1408  34092  bnj1444  34099  bnj1445  34100  bnj1446  34101  bnj1449  34104  bnj1467  34110  bnj1463  34111  bnj1489  34112  bnj1491  34113  bnj1312  34114  bnj1525  34125  bj-axrep3  34376  bj-axrep4  34377  bj-axrep5  34378  riotasv2d  34688  riotasv2s  34689  glbconxN  35102  pmapglb2xN  35496  cdlemefs32sn1aw  36140
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-12 1854
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-nf 1617
  Copyright terms: Public domain W3C validator