Theorem nffvmpt1 6853

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

Syntax hints:  Ⅎwnfc 2884   ↦ cmpt 5181  ‘cfv 6500

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-iota 6456  df-fv 6508

This theorem is referenced by:  fvmptt  6970  fmptco  7084  offval2f  7647  offval2  7652  ofrfval2  7653  mptelixpg  8885  dom2lem  8941  cantnflem1  9610  acni2  9968  axcc2  10359  seqof2  13995  rlim2  15431  ello1mpt  15456  o1compt  15522  sumfc  15644  fsum  15655  fsumf1o  15658  sumss  15659  fsumcvg2  15662  fsumadd  15675  isummulc2  15697  fsummulc2  15719  fsumrelem  15742  isumshft  15774  zprod  15872  fprod  15876  prodfc  15880  fprodf1o  15881  fprodmul  15895  fproddiv  15896  iserodd  16775  prdsbas3  17413  prdsdsval2  17416  invfuc  17913  yonedalem4b  18211  gsumdixp  20266  evlslem4  22043  elptr2  23530  ptunimpt  23551  ptcldmpt  23570  ptclsg  23571  txcnp  23576  ptcnplem  23577  cnmpt1t  23621  cnmptk2  23642  flfcnp2  23963  voliun  25523  mbfeqalem1  25610  mbfpos  25620  mbfposb  25622  mbfsup  25633  mbfinf  25634  mbflim  25637  i1fposd  25676  isibl2  25735  itgmpt  25752  itgeqa  25783  itggt0  25813  itgcn  25814  limcmpt  25852  lhop2  25988  itgsubstlem  26023  itgsubst  26024  elplyd  26175  coeeq2  26215  dgrle  26216  ulmss  26374  itgulm2  26386  leibpi  26920  rlimcnp  26943  o1cxp  26953  lgamgulmlem2  27008  lgamgulmlem6  27012  fmptcof2  32747  itggt0cn  37941  elrfirn2  43053  eq0rabdioph  43133  monotoddzz  43300  aomclem8  43418  fmuldfeq  45943  vonioo  47040