Theorem nffvmpt1 6902

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

Syntax hints:  Ⅎwnfc 2883   ↦ cmpt 5231  ‘cfv 6543

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-iota 6495  df-fv 6551

This theorem is referenced by:  fvmptt  7018  fmptco  7129  offval2f  7687  offval2  7692  ofrfval2  7693  mptelixpg  8931  dom2lem  8990  cantnflem1  9686  acni2  10043  axcc2  10434  seqof2  14028  rlim2  15442  ello1mpt  15467  o1compt  15533  sumfc  15657  fsum  15668  fsumf1o  15671  sumss  15672  fsumcvg2  15675  fsumadd  15688  isummulc2  15710  fsummulc2  15732  fsumrelem  15755  isumshft  15787  zprod  15883  fprod  15887  prodfc  15891  fprodf1o  15892  fprodmul  15906  fproddiv  15907  iserodd  16770  prdsbas3  17429  prdsdsval2  17432  invfuc  17929  yonedalem4b  18231  gsumdixp  20135  evlslem4  21643  elptr2  23085  ptunimpt  23106  ptcldmpt  23125  ptclsg  23126  txcnp  23131  ptcnplem  23132  cnmpt1t  23176  cnmptk2  23197  flfcnp2  23518  voliun  25078  mbfeqalem1  25165  mbfpos  25175  mbfposb  25177  mbfsup  25188  mbfinf  25189  mbflim  25192  i1fposd  25232  isibl2  25291  itgmpt  25307  itgeqa  25338  itggt0  25368  itgcn  25369  limcmpt  25407  lhop2  25539  itgsubstlem  25572  itgsubst  25573  elplyd  25723  coeeq2  25763  dgrle  25764  ulmss  25916  itgulm2  25928  leibpi  26454  rlimcnp  26477  o1cxp  26486  lgamgulmlem2  26541  lgamgulmlem6  26545  fmptcof2  31920  itggt0cn  36644  elrfirn2  41516  eq0rabdioph  41596  monotoddzz  41764  aomclem8  41885  fmuldfeq  44378  vonioo  45477