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

Theorem nffvmpt1 6237
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 4780 . 2 𝑥(𝑥𝐴𝐵)
2 nfcv 2793 . 2 𝑥𝐶
31, 2nffv 6236 1 𝑥((𝑥𝐴𝐵)‘𝐶)
Colors of variables: wff setvar class
Syntax hints:  wnfc 2780  cmpt 4762  cfv 5926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-iota 5889  df-fv 5934
This theorem is referenced by:  fvmptt  6339  fmptco  6436  offval2f  6951  offval2  6956  ofrfval2  6957  mptelixpg  7987  dom2lem  8037  cantnflem1  8624  acni2  8907  axcc2  9297  seqof2  12899  rlim2  14271  ello1mpt  14296  o1compt  14362  sumfc  14484  fsum  14495  fsumf1o  14498  sumss  14499  fsumcvg2  14502  fsumadd  14514  isummulc2  14537  fsummulc2  14560  fsumrelem  14583  isumshft  14615  zprod  14711  fprod  14715  prodfc  14719  fprodf1o  14720  fprodmul  14734  fproddiv  14735  iserodd  15587  prdsbas3  16188  prdsdsval2  16191  invfuc  16681  yonedalem4b  16963  gsumdixp  18655  evlslem4  19556  elptr2  21425  ptunimpt  21446  ptcldmpt  21465  ptclsg  21466  txcnp  21471  ptcnplem  21472  cnmpt1t  21516  cnmptk2  21537  flfcnp2  21858  voliun  23368  mbfeqalem  23454  mbfpos  23463  mbfposb  23465  mbfsup  23476  mbfinf  23477  mbflim  23480  i1fposd  23519  isibl2  23578  itgmpt  23594  itgeqa  23625  itggt0  23653  itgcn  23654  limcmpt  23692  lhop2  23823  itgsubstlem  23856  itgsubst  23857  elplyd  24003  coeeq2  24043  dgrle  24044  ulmss  24196  itgulm2  24208  leibpi  24714  rlimcnp  24737  o1cxp  24746  lgamgulmlem2  24801  lgamgulmlem6  24805  fmptcof2  29585  itggt0cn  33612  elrfirn2  37576  eq0rabdioph  37657  monotoddzz  37825  aomclem8  37948  fmuldfeq  40133  vonioo  41217
  Copyright terms: Public domain W3C validator