Theorem nffvmpt1 6656

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

Syntax hints:  Ⅎwnfc 2936   ↦ cmpt 5110  ‘cfv 6324

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-iota 6283  df-fv 6332

This theorem is referenced by:  fvmptt  6765  fmptco  6868  offval2f  7401  offval2  7406  ofrfval2  7407  mptelixpg  8482  dom2lem  8532  cantnflem1  9136  acni2  9457  axcc2  9848  seqof2  13424  rlim2  14845  ello1mpt  14870  o1compt  14936  sumfc  15058  fsum  15069  fsumf1o  15072  sumss  15073  fsumcvg2  15076  fsumadd  15088  isummulc2  15109  fsummulc2  15131  fsumrelem  15154  isumshft  15186  zprod  15283  fprod  15287  prodfc  15291  fprodf1o  15292  fprodmul  15306  fproddiv  15307  iserodd  16162  prdsbas3  16746  prdsdsval2  16749  invfuc  17236  yonedalem4b  17518  gsumdixp  19355  evlslem4  20747  elptr2  22179  ptunimpt  22200  ptcldmpt  22219  ptclsg  22220  txcnp  22225  ptcnplem  22226  cnmpt1t  22270  cnmptk2  22291  flfcnp2  22612  voliun  24158  mbfeqalem1  24245  mbfpos  24255  mbfposb  24257  mbfsup  24268  mbfinf  24269  mbflim  24272  i1fposd  24311  isibl2  24370  itgmpt  24386  itgeqa  24417  itggt0  24447  itgcn  24448  limcmpt  24486  lhop2  24618  itgsubstlem  24651  itgsubst  24652  elplyd  24799  coeeq2  24839  dgrle  24840  ulmss  24992  itgulm2  25004  leibpi  25528  rlimcnp  25551  o1cxp  25560  lgamgulmlem2  25615  lgamgulmlem6  25619  fmptcof2  30420  itggt0cn  35127  elrfirn2  39637  eq0rabdioph  39717  monotoddzz  39884  aomclem8  40005  fmuldfeq  42225  vonioo  43321