Theorem nffvmpt1 6869

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

Syntax hints:  Ⅎwnfc 2876   ↦ cmpt 5188  ‘cfv 6511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-iota 6464  df-fv 6519

This theorem is referenced by:  fvmptt  6988  fmptco  7101  offval2f  7668  offval2  7673  ofrfval2  7674  mptelixpg  8908  dom2lem  8963  cantnflem1  9642  acni2  9999  axcc2  10390  seqof2  14025  rlim2  15462  ello1mpt  15487  o1compt  15553  sumfc  15675  fsum  15686  fsumf1o  15689  sumss  15690  fsumcvg2  15693  fsumadd  15706  isummulc2  15728  fsummulc2  15750  fsumrelem  15773  isumshft  15805  zprod  15903  fprod  15907  prodfc  15911  fprodf1o  15912  fprodmul  15926  fproddiv  15927  iserodd  16806  prdsbas3  17444  prdsdsval2  17447  invfuc  17939  yonedalem4b  18237  gsumdixp  20228  evlslem4  21983  elptr2  23461  ptunimpt  23482  ptcldmpt  23501  ptclsg  23502  txcnp  23507  ptcnplem  23508  cnmpt1t  23552  cnmptk2  23573  flfcnp2  23894  voliun  25455  mbfeqalem1  25542  mbfpos  25552  mbfposb  25554  mbfsup  25565  mbfinf  25566  mbflim  25569  i1fposd  25608  isibl2  25667  itgmpt  25684  itgeqa  25715  itggt0  25745  itgcn  25746  limcmpt  25784  lhop2  25920  itgsubstlem  25955  itgsubst  25956  elplyd  26107  coeeq2  26147  dgrle  26148  ulmss  26306  itgulm2  26318  leibpi  26852  rlimcnp  26875  o1cxp  26885  lgamgulmlem2  26940  lgamgulmlem6  26944  fmptcof2  32581  itggt0cn  37684  elrfirn2  42684  eq0rabdioph  42764  monotoddzz  42932  aomclem8  43050  fmuldfeq  45581  vonioo  46680