Theorem nffvmpt1 6908

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

Syntax hints:  Ⅎwnfc 2879   ↦ cmpt 5231  ‘cfv 6548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ral 3059  df-rex 3068  df-rab 3430  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-iota 6500  df-fv 6556

This theorem is referenced by:  fvmptt  7025  fmptco  7138  offval2f  7700  offval2  7705  ofrfval2  7706  mptelixpg  8953  dom2lem  9012  cantnflem1  9712  acni2  10069  axcc2  10460  seqof2  14057  rlim2  15472  ello1mpt  15497  o1compt  15563  sumfc  15687  fsum  15698  fsumf1o  15701  sumss  15702  fsumcvg2  15705  fsumadd  15718  isummulc2  15740  fsummulc2  15762  fsumrelem  15785  isumshft  15817  zprod  15913  fprod  15917  prodfc  15921  fprodf1o  15922  fprodmul  15936  fproddiv  15937  iserodd  16803  prdsbas3  17462  prdsdsval2  17465  invfuc  17965  yonedalem4b  18267  gsumdixp  20254  evlslem4  22019  elptr2  23477  ptunimpt  23498  ptcldmpt  23517  ptclsg  23518  txcnp  23523  ptcnplem  23524  cnmpt1t  23568  cnmptk2  23589  flfcnp2  23910  voliun  25482  mbfeqalem1  25569  mbfpos  25579  mbfposb  25581  mbfsup  25592  mbfinf  25593  mbflim  25596  i1fposd  25636  isibl2  25695  itgmpt  25711  itgeqa  25742  itggt0  25772  itgcn  25773  limcmpt  25811  lhop2  25947  itgsubstlem  25982  itgsubst  25983  elplyd  26135  coeeq2  26175  dgrle  26176  ulmss  26332  itgulm2  26344  leibpi  26873  rlimcnp  26896  o1cxp  26906  lgamgulmlem2  26961  lgamgulmlem6  26965  fmptcof2  32442  itggt0cn  37163  elrfirn2  42116  eq0rabdioph  42196  monotoddzz  42364  aomclem8  42485  fmuldfeq  44971  vonioo  46070