Theorem nffvmpt1 6838

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

Syntax hints:  Ⅎwnfc 2886   ↦ cmpt 5153  ‘cfv 6485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-mpt 5154  df-iota 6441  df-fv 6493

This theorem is referenced by:  fvmptt  6956  fmptco  7071  offval2f  7635  offval2  7640  ofrfval2  7641  mptelixpg  8873  dom2lem  8929  cantnflem1  9601  acni2  9959  axcc2  10350  seqof2  14013  rlim2  15449  ello1mpt  15474  o1compt  15540  sumfc  15662  fsum  15673  fsumf1o  15676  sumss  15677  fsumcvg2  15680  fsumadd  15693  isummulc2  15715  fsummulc2  15737  fsumrelem  15761  isumshft  15795  zprod  15893  fprod  15897  prodfc  15901  fprodf1o  15902  fprodmul  15916  fproddiv  15917  iserodd  16797  prdsbas3  17435  prdsdsval2  17438  invfuc  17935  yonedalem4b  18233  gsumdixp  20289  evlslem4  22052  elptr2  23557  ptunimpt  23578  ptcldmpt  23597  ptclsg  23598  txcnp  23603  ptcnplem  23604  cnmpt1t  23648  cnmptk2  23669  flfcnp2  23990  voliun  25539  mbfeqalem1  25626  mbfpos  25636  mbfposb  25638  mbfsup  25649  mbfinf  25650  mbflim  25653  i1fposd  25692  isibl2  25751  itgmpt  25768  itgeqa  25799  itggt0  25829  itgcn  25830  limcmpt  25868  lhop2  26000  itgsubstlem  26033  itgsubst  26034  elplyd  26185  coeeq2  26225  dgrle  26226  ulmss  26380  itgulm2  26392  leibpi  26924  rlimcnp  26947  o1cxp  26956  lgamgulmlem2  27011  lgamgulmlem6  27015  fmptcof2  32749  itggt0cn  38057  elrfirn2  43145  eq0rabdioph  43225  monotoddzz  43388  aomclem8  43506  fmuldfeq  46028  vonioo  47125