Theorem nffvmpt1 6851

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

Syntax hints:  Ⅎwnfc 2876   ↦ cmpt 5183  ‘cfv 6499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-iota 6452  df-fv 6507

This theorem is referenced by:  fvmptt  6970  fmptco  7083  offval2f  7648  offval2  7653  ofrfval2  7654  mptelixpg  8885  dom2lem  8940  cantnflem1  9618  acni2  9975  axcc2  10366  seqof2  14001  rlim2  15438  ello1mpt  15463  o1compt  15529  sumfc  15651  fsum  15662  fsumf1o  15665  sumss  15666  fsumcvg2  15669  fsumadd  15682  isummulc2  15704  fsummulc2  15726  fsumrelem  15749  isumshft  15781  zprod  15879  fprod  15883  prodfc  15887  fprodf1o  15888  fprodmul  15902  fproddiv  15903  iserodd  16782  prdsbas3  17420  prdsdsval2  17423  invfuc  17915  yonedalem4b  18213  gsumdixp  20204  evlslem4  21959  elptr2  23437  ptunimpt  23458  ptcldmpt  23477  ptclsg  23478  txcnp  23483  ptcnplem  23484  cnmpt1t  23528  cnmptk2  23549  flfcnp2  23870  voliun  25431  mbfeqalem1  25518  mbfpos  25528  mbfposb  25530  mbfsup  25541  mbfinf  25542  mbflim  25545  i1fposd  25584  isibl2  25643  itgmpt  25660  itgeqa  25691  itggt0  25721  itgcn  25722  limcmpt  25760  lhop2  25896  itgsubstlem  25931  itgsubst  25932  elplyd  26083  coeeq2  26123  dgrle  26124  ulmss  26282  itgulm2  26294  leibpi  26828  rlimcnp  26851  o1cxp  26861  lgamgulmlem2  26916  lgamgulmlem6  26920  fmptcof2  32554  itggt0cn  37657  elrfirn2  42657  eq0rabdioph  42737  monotoddzz  42905  aomclem8  43023  fmuldfeq  45554  vonioo  46653