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

Theorem nffvmpt1 6733
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 5158 . 2 𝑥(𝑥𝐴𝐵)
2 nfcv 2904 . 2 𝑥𝐶
31, 2nffv 6732 1 𝑥((𝑥𝐴𝐵)‘𝐶)
Colors of variables: wff setvar class
Syntax hints:  wnfc 2884  cmpt 5140  cfv 6385
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3415  df-dif 3874  df-un 3876  df-in 3878  df-ss 3888  df-nul 4243  df-if 4445  df-sn 4547  df-pr 4549  df-op 4553  df-uni 4825  df-br 5059  df-opab 5121  df-mpt 5141  df-iota 6343  df-fv 6393
This theorem is referenced by:  fvmptt  6843  fmptco  6949  offval2f  7488  offval2  7493  ofrfval2  7494  mptelixpg  8621  dom2lem  8673  cantnflem1  9309  acni2  9665  axcc2  10056  seqof2  13639  rlim2  15062  ello1mpt  15087  o1compt  15153  sumfc  15278  fsum  15289  fsumf1o  15292  sumss  15293  fsumcvg2  15296  fsumadd  15309  isummulc2  15331  fsummulc2  15353  fsumrelem  15376  isumshft  15408  zprod  15504  fprod  15508  prodfc  15512  fprodf1o  15513  fprodmul  15527  fproddiv  15528  iserodd  16393  prdsbas3  16991  prdsdsval2  16994  invfuc  17488  yonedalem4b  17789  gsumdixp  19632  evlslem4  21039  elptr2  22476  ptunimpt  22497  ptcldmpt  22516  ptclsg  22517  txcnp  22522  ptcnplem  22523  cnmpt1t  22567  cnmptk2  22588  flfcnp2  22909  voliun  24456  mbfeqalem1  24543  mbfpos  24553  mbfposb  24555  mbfsup  24566  mbfinf  24567  mbflim  24570  i1fposd  24610  isibl2  24669  itgmpt  24685  itgeqa  24716  itggt0  24746  itgcn  24747  limcmpt  24785  lhop2  24917  itgsubstlem  24950  itgsubst  24951  elplyd  25101  coeeq2  25141  dgrle  25142  ulmss  25294  itgulm2  25306  leibpi  25830  rlimcnp  25853  o1cxp  25862  lgamgulmlem2  25917  lgamgulmlem6  25921  fmptcof2  30719  itggt0cn  35589  elrfirn2  40229  eq0rabdioph  40309  monotoddzz  40476  aomclem8  40597  fmuldfeq  42807  vonioo  43903
  Copyright terms: Public domain W3C validator