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

Theorem nffvmpt1 6096
Description: Bound-variable hypothesis builder for mapping, special case. (Contributed by Mario Carneiro, 25-Dec-2016.)
Assertion
Ref Expression
nffvmpt1 𝑥((𝑥𝐴𝐵)‘𝐶)
Distinct variable group:   𝑥,𝐶
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)

Proof of Theorem nffvmpt1
StepHypRef Expression
1 nfmpt1 4670 . 2 𝑥(𝑥𝐴𝐵)
2 nfcv 2751 . 2 𝑥𝐶
31, 2nffv 6095 1 𝑥((𝑥𝐴𝐵)‘𝐶)
Colors of variables: wff setvar class
Syntax hints:  wnfc 2738  cmpt 4638  cfv 5790
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4368  df-br 4579  df-opab 4639  df-mpt 4640  df-iota 5754  df-fv 5798
This theorem is referenced by:  fvmptt  6193  fmptco  6288  offval2f  6785  offval2  6790  ofrfval2  6791  mptelixpg  7809  dom2lem  7859  cantnflem1  8447  acni2  8730  axcc2  9120  seqof2  12679  rlim2  14024  ello1mpt  14049  o1compt  14115  sumfc  14236  fsum  14247  fsumf1o  14250  sumss  14251  fsumcvg2  14254  fsumadd  14266  isummulc2  14284  fsummulc2  14307  fsumrelem  14329  isumshft  14359  zprod  14455  fprod  14459  prodfc  14463  fprodf1o  14464  fprodmul  14478  fproddiv  14479  iserodd  15327  prdsbas3  15913  prdsdsval2  15916  invfuc  16406  yonedalem4b  16688  gsumdixp  18381  evlslem4  19278  elptr2  21135  ptunimpt  21156  ptcldmpt  21175  ptclsg  21176  txcnp  21181  ptcnplem  21182  cnmpt1t  21226  cnmptk2  21247  flfcnp2  21569  voliun  23074  mbfeqalem  23160  mbfpos  23169  mbfposb  23171  mbfsup  23182  mbfinf  23183  mbflim  23186  i1fposd  23225  isibl2  23284  itgmpt  23300  itgeqa  23331  itggt0  23359  itgcn  23360  limcmpt  23398  lhop2  23527  itgsubstlem  23560  itgsubst  23561  elplyd  23707  coeeq2  23747  dgrle  23748  ulmss  23900  itgulm2  23912  leibpi  24414  rlimcnp  24437  o1cxp  24446  lgamgulmlem2  24501  lgamgulmlem6  24505  fmptcof2  28633  itggt0cn  32446  elrfirn2  36071  eq0rabdioph  36152  monotoddzz  36320  aomclem8  36443  fmuldfeq  38444  vonioo  39367
  Copyright terms: Public domain W3C validator