Theorem nffvmpt1 6890

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

Syntax hints:  Ⅎwnfc 2916   ↦ cmpt 5193  ‘cfv 6534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-iota 6490  df-fv 6542

This theorem is referenced by:  fvmptt  7008  fmptco  7123  offval2f  7687  offval2  7692  ofrfval2  7693  mptelixpg  8929  dom2lem  8985  cantnflem1  9654  acni2  10026  axcc2  10417  seqof2  14092  rlim2  15543  ello1mpt  15568  o1compt  15634  sumfc  15756  fsum  15767  fsumf1o  15770  sumss  15771  fsumcvg2  15774  fsumadd  15787  isummulc2  15809  fsummulc2  15831  fsumrelem  15855  isumshft  15889  zprod  15987  fprod  15991  prodfc  15995  fprodf1o  15996  fprodmul  16010  fproddiv  16011  iserodd  16891  prdsbas3  17530  prdsdsval2  17533  invfuc  18030  yonedalem4b  18328  gsumdixp  20396  evlslem4  22192  elptr2  23696  ptunimpt  23717  ptcldmpt  23736  ptclsg  23737  txcnp  23742  ptcnplem  23743  cnmpt1t  23787  cnmptk2  23808  flfcnp2  24129  voliun  25678  mbfeqalem1  25765  mbfpos  25775  mbfposb  25777  mbfsup  25788  mbfinf  25789  mbflim  25792  i1fposd  25831  isibl2  25890  itgmpt  25907  itgeqa  25938  itggt0  25968  itgcn  25969  limcmpt  26007  lhop2  26139  itgsubstlem  26172  itgsubst  26173  elplyd  26324  coeeq2  26364  dgrle  26365  ulmss  26522  itgulm2  26534  leibpi  27069  rlimcnp  27092  o1cxp  27101  lgamgulmlem2  27156  lgamgulmlem6  27160  fmptcof2  32939  itggt0cn  38224  elrfirn2  43314  eq0rabdioph  43394  monotoddzz  43557  aomclem8  43675  fmuldfeq  46186  vonioo  47283