Theorem nffvmpt1 6917

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 5250	. 2 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵)
2		nfcv 2905	. 2 ⊢ Ⅎ𝑥𝐶
3	1, 2	nffv 6916	1 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝐶)

Syntax hints:  Ⅎwnfc 2890   ↦ cmpt 5225  ‘cfv 6561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-iota 6514  df-fv 6569

This theorem is referenced by:  fvmptt  7036  fmptco  7149  offval2f  7712  offval2  7717  ofrfval2  7718  mptelixpg  8975  dom2lem  9032  cantnflem1  9729  acni2  10086  axcc2  10477  seqof2  14101  rlim2  15532  ello1mpt  15557  o1compt  15623  sumfc  15745  fsum  15756  fsumf1o  15759  sumss  15760  fsumcvg2  15763  fsumadd  15776  isummulc2  15798  fsummulc2  15820  fsumrelem  15843  isumshft  15875  zprod  15973  fprod  15977  prodfc  15981  fprodf1o  15982  fprodmul  15996  fproddiv  15997  iserodd  16873  prdsbas3  17526  prdsdsval2  17529  invfuc  18022  yonedalem4b  18321  gsumdixp  20316  evlslem4  22100  elptr2  23582  ptunimpt  23603  ptcldmpt  23622  ptclsg  23623  txcnp  23628  ptcnplem  23629  cnmpt1t  23673  cnmptk2  23694  flfcnp2  24015  voliun  25589  mbfeqalem1  25676  mbfpos  25686  mbfposb  25688  mbfsup  25699  mbfinf  25700  mbflim  25703  i1fposd  25742  isibl2  25801  itgmpt  25818  itgeqa  25849  itggt0  25879  itgcn  25880  limcmpt  25918  lhop2  26054  itgsubstlem  26089  itgsubst  26090  elplyd  26241  coeeq2  26281  dgrle  26282  ulmss  26440  itgulm2  26452  leibpi  26985  rlimcnp  27008  o1cxp  27018  lgamgulmlem2  27073  lgamgulmlem6  27077  fmptcof2  32667  itggt0cn  37697  elrfirn2  42707  eq0rabdioph  42787  monotoddzz  42955  aomclem8  43073  fmuldfeq  45598  vonioo  46697