Theorem nffvmpt1 6845

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

Syntax hints:  Ⅎwnfc 2883   ↦ cmpt 5179  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-iota 6448  df-fv 6500

This theorem is referenced by:  fvmptt  6961  fmptco  7074  offval2f  7637  offval2  7642  ofrfval2  7643  mptelixpg  8873  dom2lem  8929  cantnflem1  9598  acni2  9956  axcc2  10347  seqof2  13983  rlim2  15419  ello1mpt  15444  o1compt  15510  sumfc  15632  fsum  15643  fsumf1o  15646  sumss  15647  fsumcvg2  15650  fsumadd  15663  isummulc2  15685  fsummulc2  15707  fsumrelem  15730  isumshft  15762  zprod  15860  fprod  15864  prodfc  15868  fprodf1o  15869  fprodmul  15883  fproddiv  15884  iserodd  16763  prdsbas3  17401  prdsdsval2  17404  invfuc  17901  yonedalem4b  18199  gsumdixp  20254  evlslem4  22031  elptr2  23518  ptunimpt  23539  ptcldmpt  23558  ptclsg  23559  txcnp  23564  ptcnplem  23565  cnmpt1t  23609  cnmptk2  23630  flfcnp2  23951  voliun  25511  mbfeqalem1  25598  mbfpos  25608  mbfposb  25610  mbfsup  25621  mbfinf  25622  mbflim  25625  i1fposd  25664  isibl2  25723  itgmpt  25740  itgeqa  25771  itggt0  25801  itgcn  25802  limcmpt  25840  lhop2  25976  itgsubstlem  26011  itgsubst  26012  elplyd  26163  coeeq2  26203  dgrle  26204  ulmss  26362  itgulm2  26374  leibpi  26908  rlimcnp  26931  o1cxp  26941  lgamgulmlem2  26996  lgamgulmlem6  27000  fmptcof2  32735  itggt0cn  37891  elrfirn2  42938  eq0rabdioph  43018  monotoddzz  43185  aomclem8  43303  fmuldfeq  45829  vonioo  46926