Theorem nffvmpt1 6896

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

This proof depends on syntax axioms:  Ⅎwnfc 2912   ↦ cmpt 5194  ‘cfv 6540

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-iota 6496  df-fv 6548

This theorem is used by:  fvmptt  7014  fmptco  7129  offval2f  7695  offval2  7700  ofrfval2  7701  mptelixpg  8935  dom2lem  8991  cantnflem1  9661  acni2  10042  axcc2  10432  seqof2  14110  rlim2  15567  ello1mpt  15592  o1compt  15658  sumfc  15779  fsum  15790  fsumf1o  15793  sumss  15794  fsumcvg2  15797  fsumadd  15810  isummulc2  15832  fsummulc2  15854  fsumrelem  15878  isumshft  15912  zprod  16010  fprod  16014  prodfc  16018  fprodf1o  16019  fprodmul  16033  fproddiv  16034  iserodd  16913  prdsbas3  17552  prdsdsval2  17555  invfuc  18052  yonedalem4b  18350  gsumdixp  20426  evlslem4  22257  elptr2  23762  ptunimpt  23783  ptcldmpt  23802  ptclsg  23803  txcnp  23808  ptcnplem  23809  cnmpt1t  23853  cnmptk2  23874  flfcnp2  24195  voliun  25744  mbfeqalem1  25831  mbfpos  25841  mbfposb  25843  mbfsup  25854  mbfinf  25855  mbflim  25858  i1fposd  25897  isibl2  25956  itgmpt  25973  itgeqa  26004  itggt0  26034  itgcn  26035  limcmpt  26073  lhop2  26205  itgsubstlem  26238  itgsubst  26239  elplyd  26390  coeeq2  26430  dgrle  26431  ulmss  26591  itgulm2  26603  leibpi  27138  rlimcnp  27161  o1cxp  27170  lgamgulmlem2  27225  lgamgulmlem6  27229  fmptcof2  33049  itggt0cn  38374  elrfirn2  43460  eq0rabdioph  43540  monotoddzz  43703  aomclem8  43821  fmuldfeq  46332  vonioo  47429