Theorem nffvmpt1 6445

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

Syntax hints:  Ⅎwnfc 2957   ↦ cmpt 4953  ‘cfv 6124

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2804

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2813  df-cleq 2819  df-clel 2822  df-nfc 2959  df-ral 3123  df-rex 3124  df-rab 3127  df-v 3417  df-dif 3802  df-un 3804  df-in 3806  df-ss 3813  df-nul 4146  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4660  df-br 4875  df-opab 4937  df-mpt 4954  df-iota 6087  df-fv 6132

This theorem is referenced by:  fvmptt  6548  fmptco  6647  offval2f  7170  offval2  7175  ofrfval2  7176  mptelixpg  8213  dom2lem  8263  cantnflem1  8864  acni2  9183  axcc2  9575  seqof2  13154  rlim2  14605  ello1mpt  14630  o1compt  14696  sumfc  14818  fsum  14829  fsumf1o  14832  sumss  14833  fsumcvg2  14836  fsumadd  14848  isummulc2  14869  fsummulc2  14891  fsumrelem  14914  isumshft  14946  zprod  15041  fprod  15045  prodfc  15049  fprodf1o  15050  fprodmul  15064  fproddiv  15065  iserodd  15912  prdsbas3  16495  prdsdsval2  16498  invfuc  16987  yonedalem4b  17270  gsumdixp  18964  evlslem4  19869  elptr2  21749  ptunimpt  21770  ptcldmpt  21789  ptclsg  21790  txcnp  21795  ptcnplem  21796  cnmpt1t  21840  cnmptk2  21861  flfcnp2  22182  voliun  23721  mbfeqalem1  23808  mbfpos  23818  mbfposb  23820  mbfsup  23831  mbfinf  23832  mbflim  23835  i1fposd  23874  isibl2  23933  itgmpt  23949  itgeqa  23980  itggt0  24008  itgcn  24009  limcmpt  24047  lhop2  24178  itgsubstlem  24211  itgsubst  24212  elplyd  24358  coeeq2  24398  dgrle  24399  ulmss  24551  itgulm2  24563  leibpi  25083  rlimcnp  25106  o1cxp  25115  lgamgulmlem2  25170  lgamgulmlem6  25174  fmptcof2  30007  itggt0cn  34026  elrfirn2  38104  eq0rabdioph  38185  monotoddzz  38352  aomclem8  38475  fmuldfeq  40611  vonioo  41691