Theorem nffvmpt1 6845

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

Syntax hints:  Ⅎwnfc 2884   ↦ cmpt 5167  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-iota 6448  df-fv 6500

This theorem is referenced by:  fvmptt  6962  fmptco  7076  offval2f  7639  offval2  7644  ofrfval2  7645  mptelixpg  8876  dom2lem  8932  cantnflem1  9601  acni2  9959  axcc2  10350  seqof2  14013  rlim2  15449  ello1mpt  15474  o1compt  15540  sumfc  15662  fsum  15673  fsumf1o  15676  sumss  15677  fsumcvg2  15680  fsumadd  15693  isummulc2  15715  fsummulc2  15737  fsumrelem  15761  isumshft  15795  zprod  15893  fprod  15897  prodfc  15901  fprodf1o  15902  fprodmul  15916  fproddiv  15917  iserodd  16797  prdsbas3  17435  prdsdsval2  17438  invfuc  17935  yonedalem4b  18233  gsumdixp  20289  evlslem4  22064  elptr2  23549  ptunimpt  23570  ptcldmpt  23589  ptclsg  23590  txcnp  23595  ptcnplem  23596  cnmpt1t  23640  cnmptk2  23661  flfcnp2  23982  voliun  25531  mbfeqalem1  25618  mbfpos  25628  mbfposb  25630  mbfsup  25641  mbfinf  25642  mbflim  25645  i1fposd  25684  isibl2  25743  itgmpt  25760  itgeqa  25791  itggt0  25821  itgcn  25822  limcmpt  25860  lhop2  25992  itgsubstlem  26025  itgsubst  26026  elplyd  26177  coeeq2  26217  dgrle  26218  ulmss  26375  itgulm2  26387  leibpi  26919  rlimcnp  26942  o1cxp  26952  lgamgulmlem2  27007  lgamgulmlem6  27011  fmptcof2  32745  itggt0cn  38025  elrfirn2  43142  eq0rabdioph  43222  monotoddzz  43389  aomclem8  43507  fmuldfeq  46031  vonioo  47128