Theorem nffvmpt1 6894

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

This proof depends on syntax axioms:  Ⅎwnfc 2908   ↦ cmpt 5186  ‘cfv 6537

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733

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 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-iota 6493  df-fv 6545

This theorem is used by:  fvmptt  7012  fmptco  7128  offval2f  7706  offval2  7711  ofrfval2  7712  mptelixpg  8956  dom2lem  9012  cantnflem1  9683  acni2  10118  axcc2  10508  seqof2  14196  rlim2  15656  ello1mpt  15681  o1compt  15747  sumfc  15868  fsum  15879  fsumf1o  15882  sumss  15883  fsumcvg2  15886  fsumadd  15899  isummulc2  15921  fsummulc2  15943  fsumrelem  15967  isumshft  16001  zprod  16097  fprod  16101  prodfc  16105  fprodf1o  16106  fprodmul  16120  fproddiv  16121  iserodd  17006  prdsbas3  17645  prdsdsval2  17648  invfuc  18145  yonedalem4b  18443  gsumdixp  20541  evlslem4  22378  elptr2  23886  ptunimpt  23907  ptcldmpt  23926  ptclsg  23927  txcnp  23932  ptcnplem  23933  cnmpt1t  23977  cnmptk2  23998  flfcnp2  24319  voliun  25868  mbfeqalem1  25955  mbfpos  25965  mbfposb  25967  mbfsup  25978  mbfinf  25979  mbflim  25982  i1fposd  26021  isibl2  26080  itgmpt  26096  itgeqa  26127  itggt0  26157  itgcn  26158  limcmpt  26196  lhop2  26328  itgsubstlem  26361  itgsubst  26362  elplyd  26513  coeeq2  26554  dgrle  26555  ulmss  26717  itgulm2  26729  leibpi  27263  rlimcnp  27286  o1cxp  27295  lgamgulmlem2  27350  lgamgulmlem6  27354  fmptcof2  33244  itggt0cn  38588  elrfirn2  43686  eq0rabdioph  43766  monotoddzz  43929  aomclem8  44047  fmuldfeq  46564  vonioo  47661