Theorem nffvmpt1 6927

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

This proof depends on syntax axioms:  Ⅎwnfc 2911   ↦ cmpt 5192  ‘cfv 6566

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-mpt 5193  df-iota 6520  df-fv 6574

This theorem is used by:  fvmptt  7045  fmptco  7162  offval2f  7740  offval2  7745  ofrfval2  7746  mptelixpg  9001  dom2lem  9057  cantnflem1  9727  acni2  10164  axcc2  10554  seqof2  14243  rlim2  15707  ello1mpt  15732  o1compt  15798  sumfc  15919  fsum  15930  fsumf1o  15933  sumss  15934  fsumcvg2  15937  fsumadd  15950  isummulc2  15972  fsummulc2  15994  fsumrelem  16018  isumshft  16052  zprod  16148  fprod  16152  prodfc  16156  fprodf1o  16157  fprodmul  16171  fproddiv  16172  iserodd  17057  prdsbas3  17702  prdsdsval2  17705  invfuc  18202  yonedalem4b  18500  gsumdixp  20599  evlslem4  22440  elptr2  23948  ptunimpt  23969  ptcldmpt  23988  ptclsg  23989  txcnp  23994  ptcnplem  23995  cnmpt1t  24039  cnmptk2  24060  flfcnp2  24381  voliun  25930  mbfeqalem1  26017  mbfpos  26027  mbfposb  26029  mbfsup  26040  mbfinf  26041  mbflim  26044  i1fposd  26083  isibl2  26142  itgmpt  26158  itgeqa  26189  itggt0  26219  itgcn  26220  limcmpt  26258  lhop2  26390  itgsubstlem  26423  itgsubst  26424  elplyd  26575  coeeq2  26616  dgrle  26617  ulmss  26781  itgulm2  26793  leibpi  27327  rlimcnp  27350  o1cxp  27359  lgamgulmlem2  27414  lgamgulmlem6  27418  fmptcof2  33349  itggt0cn  38876  elrfirn2  43973  eq0rabdioph  44053  monotoddzz  44216  aomclem8  44329  fmuldfeq  46868  vonioo  47965