Theorem nffvmpt1 6873

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

Syntax hints:  Ⅎwnfc 2908   ↦ cmpt 5178  ‘cfv 6516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-iota 6472  df-fv 6524

This theorem is referenced by:  fvmptt  6991  fmptco  7106  offval2f  7670  offval2  7675  ofrfval2  7676  mptelixpg  8911  dom2lem  8967  cantnflem1  9638  acni2  9996  axcc2  10388  seqof2  14067  rlim2  15514  ello1mpt  15539  o1compt  15605  sumfc  15727  fsum  15738  fsumf1o  15741  sumss  15742  fsumcvg2  15745  fsumadd  15758  isummulc2  15780  fsummulc2  15802  fsumrelem  15826  isumshft  15860  zprod  15958  fprod  15962  prodfc  15966  fprodf1o  15967  fprodmul  15981  fproddiv  15982  iserodd  16862  prdsbas3  17501  prdsdsval2  17504  invfuc  18001  yonedalem4b  18299  gsumdixp  20354  evlslem4  22117  elptr2  23622  ptunimpt  23643  ptcldmpt  23662  ptclsg  23663  txcnp  23668  ptcnplem  23669  cnmpt1t  23713  cnmptk2  23734  flfcnp2  24055  voliun  25604  mbfeqalem1  25691  mbfpos  25701  mbfposb  25703  mbfsup  25714  mbfinf  25715  mbflim  25718  i1fposd  25757  isibl2  25816  itgmpt  25833  itgeqa  25864  itggt0  25894  itgcn  25895  limcmpt  25933  lhop2  26065  itgsubstlem  26098  itgsubst  26099  elplyd  26250  coeeq2  26290  dgrle  26291  ulmss  26448  itgulm2  26460  leibpi  26995  rlimcnp  27018  o1cxp  27027  lgamgulmlem2  27082  lgamgulmlem6  27086  fmptcof2  32820  itggt0cn  38150  elrfirn2  43238  eq0rabdioph  43318  monotoddzz  43481  aomclem8  43599  fmuldfeq  46120  vonioo  47217