Theorem nffvmpt1 6892

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

Syntax hints:  Ⅎwnfc 2910   ↦ cmpt 5192  ‘cfv 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-iota 6492  df-fv 6544

This theorem is referenced by:  fvmptt  7010  fmptco  7125  offval2f  7689  offval2  7694  ofrfval2  7695  mptelixpg  8929  dom2lem  8985  cantnflem1  9654  acni2  10026  axcc2  10416  seqof2  14092  rlim2  15543  ello1mpt  15568  o1compt  15634  sumfc  15756  fsum  15767  fsumf1o  15770  sumss  15771  fsumcvg2  15774  fsumadd  15787  isummulc2  15809  fsummulc2  15831  fsumrelem  15855  isumshft  15889  zprod  15987  fprod  15991  prodfc  15995  fprodf1o  15996  fprodmul  16010  fproddiv  16011  iserodd  16890  prdsbas3  17529  prdsdsval2  17532  invfuc  18029  yonedalem4b  18327  gsumdixp  20396  evlslem4  22227  elptr2  23731  ptunimpt  23752  ptcldmpt  23771  ptclsg  23772  txcnp  23777  ptcnplem  23778  cnmpt1t  23822  cnmptk2  23843  flfcnp2  24164  voliun  25713  mbfeqalem1  25800  mbfpos  25810  mbfposb  25812  mbfsup  25823  mbfinf  25824  mbflim  25827  i1fposd  25866  isibl2  25925  itgmpt  25942  itgeqa  25973  itggt0  26003  itgcn  26004  limcmpt  26042  lhop2  26174  itgsubstlem  26207  itgsubst  26208  elplyd  26359  coeeq2  26399  dgrle  26400  ulmss  26560  itgulm2  26572  leibpi  27107  rlimcnp  27130  o1cxp  27139  lgamgulmlem2  27194  lgamgulmlem6  27198  fmptcof2  33002  itggt0cn  38341  elrfirn2  43427  eq0rabdioph  43507  monotoddzz  43670  aomclem8  43788  fmuldfeq  46299  vonioo  47396