Theorem nffvmpt1 6785

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

Syntax hints:  Ⅎwnfc 2887   ↦ cmpt 5157  ‘cfv 6433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-iota 6391  df-fv 6441

This theorem is referenced by:  fvmptt  6895  fmptco  7001  offval2f  7548  offval2  7553  ofrfval2  7554  mptelixpg  8723  dom2lem  8780  cantnflem1  9447  acni2  9802  axcc2  10193  seqof2  13781  rlim2  15205  ello1mpt  15230  o1compt  15296  sumfc  15421  fsum  15432  fsumf1o  15435  sumss  15436  fsumcvg2  15439  fsumadd  15452  isummulc2  15474  fsummulc2  15496  fsumrelem  15519  isumshft  15551  zprod  15647  fprod  15651  prodfc  15655  fprodf1o  15656  fprodmul  15670  fproddiv  15671  iserodd  16536  prdsbas3  17192  prdsdsval2  17195  invfuc  17692  yonedalem4b  17994  gsumdixp  19848  evlslem4  21284  elptr2  22725  ptunimpt  22746  ptcldmpt  22765  ptclsg  22766  txcnp  22771  ptcnplem  22772  cnmpt1t  22816  cnmptk2  22837  flfcnp2  23158  voliun  24718  mbfeqalem1  24805  mbfpos  24815  mbfposb  24817  mbfsup  24828  mbfinf  24829  mbflim  24832  i1fposd  24872  isibl2  24931  itgmpt  24947  itgeqa  24978  itggt0  25008  itgcn  25009  limcmpt  25047  lhop2  25179  itgsubstlem  25212  itgsubst  25213  elplyd  25363  coeeq2  25403  dgrle  25404  ulmss  25556  itgulm2  25568  leibpi  26092  rlimcnp  26115  o1cxp  26124  lgamgulmlem2  26179  lgamgulmlem6  26183  fmptcof2  30994  itggt0cn  35847  elrfirn2  40518  eq0rabdioph  40598  monotoddzz  40765  aomclem8  40886  fmuldfeq  43124  vonioo  44220