Theorem nffvmpt1 6901

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

This proof depends on syntax axioms:  Ⅎwnfc 2907   ↦ cmpt 5185  ‘cfv 6543

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-iota 6497  df-fv 6551

This theorem is used by:  fvmptt  7019  fmptco  7135  offval2f  7712  offval2  7717  ofrfval2  7718  mptelixpg  8970  dom2lem  9026  cantnflem1  9697  acni2  10132  axcc2  10522  seqof2  14210  rlim2  15672  ello1mpt  15697  o1compt  15763  sumfc  15884  fsum  15895  fsumf1o  15898  sumss  15899  fsumcvg2  15902  fsumadd  15915  isummulc2  15937  fsummulc2  15959  fsumrelem  15983  isumshft  16017  zprod  16113  fprod  16117  prodfc  16121  fprodf1o  16122  fprodmul  16136  fproddiv  16137  iserodd  17022  prdsbas3  17661  prdsdsval2  17664  invfuc  18161  yonedalem4b  18459  gsumdixp  20557  evlslem4  22394  elptr2  23902  ptunimpt  23923  ptcldmpt  23942  ptclsg  23943  txcnp  23948  ptcnplem  23949  cnmpt1t  23993  cnmptk2  24014  flfcnp2  24335  voliun  25884  mbfeqalem1  25971  mbfpos  25981  mbfposb  25983  mbfsup  25994  mbfinf  25995  mbflim  25998  i1fposd  26037  isibl2  26096  itgmpt  26112  itgeqa  26143  itggt0  26173  itgcn  26174  limcmpt  26212  lhop2  26344  itgsubstlem  26377  itgsubst  26378  elplyd  26529  coeeq2  26570  dgrle  26571  ulmss  26733  itgulm2  26745  leibpi  27279  rlimcnp  27302  o1cxp  27311  lgamgulmlem2  27366  lgamgulmlem6  27370  fmptcof2  33302  itggt0cn  38717  elrfirn2  43816  eq0rabdioph  43896  monotoddzz  44059  aomclem8  44172  fmuldfeq  46703  vonioo  47800