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

Syntax hints:  Ⅎwnfc 2887   ↦ cmpt 5230  ‘cfv 6562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-iota 6515  df-fv 6570

This theorem is referenced by:  fvmptt  7035  fmptco  7148  offval2f  7711  offval2  7716  ofrfval2  7717  mptelixpg  8973  dom2lem  9030  cantnflem1  9726  acni2  10083  axcc2  10474  seqof2  14097  rlim2  15528  ello1mpt  15553  o1compt  15619  sumfc  15741  fsum  15752  fsumf1o  15755  sumss  15756  fsumcvg2  15759  fsumadd  15772  isummulc2  15794  fsummulc2  15816  fsumrelem  15839  isumshft  15871  zprod  15969  fprod  15973  prodfc  15977  fprodf1o  15978  fprodmul  15992  fproddiv  15993  iserodd  16868  prdsbas3  17527  prdsdsval2  17530  invfuc  18030  yonedalem4b  18332  gsumdixp  20332  evlslem4  22117  elptr2  23597  ptunimpt  23618  ptcldmpt  23637  ptclsg  23638  txcnp  23643  ptcnplem  23644  cnmpt1t  23688  cnmptk2  23709  flfcnp2  24030  voliun  25602  mbfeqalem1  25689  mbfpos  25699  mbfposb  25701  mbfsup  25712  mbfinf  25713  mbflim  25716  i1fposd  25756  isibl2  25815  itgmpt  25832  itgeqa  25863  itggt0  25893  itgcn  25894  limcmpt  25932  lhop2  26068  itgsubstlem  26103  itgsubst  26104  elplyd  26255  coeeq2  26295  dgrle  26296  ulmss  26454  itgulm2  26466  leibpi  26999  rlimcnp  27022  o1cxp  27032  lgamgulmlem2  27087  lgamgulmlem6  27091  fmptcof2  32673  itggt0cn  37676  elrfirn2  42683  eq0rabdioph  42763  monotoddzz  42931  aomclem8  43049  fmuldfeq  45538  vonioo  46637