Theorem nffvmpt1 6767

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

Step	Hyp	Ref	Expression
1		nfmpt1 5178	. 2 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵)
2		nfcv 2906	. 2 ⊢ Ⅎ𝑥𝐶
3	1, 2	nffv 6766	1 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝐶)

Syntax hints:  Ⅎwnfc 2886   ↦ cmpt 5153  ‘cfv 6418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-iota 6376  df-fv 6426

This theorem is referenced by:  fvmptt  6877  fmptco  6983  offval2f  7526  offval2  7531  ofrfval2  7532  mptelixpg  8681  dom2lem  8735  cantnflem1  9377  acni2  9733  axcc2  10124  seqof2  13709  rlim2  15133  ello1mpt  15158  o1compt  15224  sumfc  15349  fsum  15360  fsumf1o  15363  sumss  15364  fsumcvg2  15367  fsumadd  15380  isummulc2  15402  fsummulc2  15424  fsumrelem  15447  isumshft  15479  zprod  15575  fprod  15579  prodfc  15583  fprodf1o  15584  fprodmul  15598  fproddiv  15599  iserodd  16464  prdsbas3  17109  prdsdsval2  17112  invfuc  17608  yonedalem4b  17910  gsumdixp  19763  evlslem4  21194  elptr2  22633  ptunimpt  22654  ptcldmpt  22673  ptclsg  22674  txcnp  22679  ptcnplem  22680  cnmpt1t  22724  cnmptk2  22745  flfcnp2  23066  voliun  24623  mbfeqalem1  24710  mbfpos  24720  mbfposb  24722  mbfsup  24733  mbfinf  24734  mbflim  24737  i1fposd  24777  isibl2  24836  itgmpt  24852  itgeqa  24883  itggt0  24913  itgcn  24914  limcmpt  24952  lhop2  25084  itgsubstlem  25117  itgsubst  25118  elplyd  25268  coeeq2  25308  dgrle  25309  ulmss  25461  itgulm2  25473  leibpi  25997  rlimcnp  26020  o1cxp  26029  lgamgulmlem2  26084  lgamgulmlem6  26088  fmptcof2  30896  itggt0cn  35774  elrfirn2  40434  eq0rabdioph  40514  monotoddzz  40681  aomclem8  40802  fmuldfeq  43014  vonioo  44110