Theorem nffvmpt1 6837

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

Syntax hints:  Ⅎwnfc 2876   ↦ cmpt 5176  ‘cfv 6486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-mpt 5177  df-iota 6442  df-fv 6494

This theorem is referenced by:  fvmptt  6954  fmptco  7067  offval2f  7632  offval2  7637  ofrfval2  7638  mptelixpg  8869  dom2lem  8924  cantnflem1  9604  acni2  9959  axcc2  10350  seqof2  13986  rlim2  15422  ello1mpt  15447  o1compt  15513  sumfc  15635  fsum  15646  fsumf1o  15649  sumss  15650  fsumcvg2  15653  fsumadd  15666  isummulc2  15688  fsummulc2  15710  fsumrelem  15733  isumshft  15765  zprod  15863  fprod  15867  prodfc  15871  fprodf1o  15872  fprodmul  15886  fproddiv  15887  iserodd  16766  prdsbas3  17404  prdsdsval2  17407  invfuc  17903  yonedalem4b  18201  gsumdixp  20223  evlslem4  22000  elptr2  23478  ptunimpt  23499  ptcldmpt  23518  ptclsg  23519  txcnp  23524  ptcnplem  23525  cnmpt1t  23569  cnmptk2  23590  flfcnp2  23911  voliun  25472  mbfeqalem1  25559  mbfpos  25569  mbfposb  25571  mbfsup  25582  mbfinf  25583  mbflim  25586  i1fposd  25625  isibl2  25684  itgmpt  25701  itgeqa  25732  itggt0  25762  itgcn  25763  limcmpt  25801  lhop2  25937  itgsubstlem  25972  itgsubst  25973  elplyd  26124  coeeq2  26164  dgrle  26165  ulmss  26323  itgulm2  26335  leibpi  26869  rlimcnp  26892  o1cxp  26902  lgamgulmlem2  26957  lgamgulmlem6  26961  fmptcof2  32619  itggt0cn  37689  elrfirn2  42689  eq0rabdioph  42769  monotoddzz  42936  aomclem8  43054  fmuldfeq  45584  vonioo  46683