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

Theorem nffvmpt1 5879
Description: Bound-variable hypothesis builder for mapping, special case. (Contributed by Mario Carneiro, 25-Dec-2016.)
Assertion
Ref Expression
nffvmpt1
Distinct variable group:   ,

Proof of Theorem nffvmpt1
StepHypRef Expression
1 nfmpt1 4541 . 2
2 nfcv 2619 . 2
31, 2nffv 5878 1
Colors of variables: wff setvar class
Syntax hints:  F/_wnfc 2605  e.cmpt 4510  `cfv 5593
This theorem is referenced by:  fvmptt  5971  fmptco  6064  offval2  6556  ofrfval2  6557  mptelixpg  7526  dom2lem  7575  cantnflem1  8129  acni2  8448  axcc2  8838  seqof2  12165  rlim2  13319  ello1mpt  13344  o1compt  13410  sumfc  13531  fsum  13542  fsumf1o  13545  sumss  13546  fsumcvg2  13549  fsumadd  13561  isummulc2  13577  fsummulc2  13599  fsumrelem  13621  isumshft  13651  zprod  13744  fprod  13748  prodfc  13752  fprodf1o  13753  fprodmul  13765  fproddiv  13766  iserodd  14359  prdsbas3  14878  prdsdsval2  14881  invfuc  15343  yonedalem4b  15545  dprdwdOLD2  17045  dprdwdOLD  17051  gsumdixpOLD  17257  gsumdixp  17258  evlslem4OLD  18173  evlslem4  18174  elptr2  20075  ptunimpt  20096  ptcldmpt  20115  ptclsg  20116  txcnp  20121  ptcnplem  20122  cnmpt1t  20166  cnmptk2  20187  flfcnp2  20508  voliun  21964  mbfeqalem  22049  mbfpos  22058  mbfposb  22060  mbfsup  22071  mbfinf  22072  mbflim  22075  i1fposd  22114  isibl2  22173  itgmpt  22189  itgeqa  22220  itggt0  22248  itgcn  22249  limcmpt  22287  lhop2  22416  itgsubstlem  22449  itgsubst  22450  elplyd  22599  coeeq2  22639  dgrle  22640  ulmss  22792  itgulm2  22804  leibpi  23273  rlimcnp  23295  o1cxp  23304  fmptcof2  27502  offval2f  27506  lgamgulmlem2  28572  lgamgulmlem6  28576  itggt0cn  30087  elrfirn2  30628  eq0rabdioph  30710  monotoddzz  30879  aomclem8  31007  fmuldfeq  31577
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-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-mpt 4512  df-iota 5556  df-fv 5601
  Copyright terms: Public domain W3C validator