Theorem nffvmpt1 6887

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

Syntax hints:  Ⅎwnfc 2883   ↦ cmpt 5201  ‘cfv 6531

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-iota 6484  df-fv 6539

This theorem is referenced by:  fvmptt  7006  fmptco  7119  offval2f  7686  offval2  7691  ofrfval2  7692  mptelixpg  8949  dom2lem  9006  cantnflem1  9703  acni2  10060  axcc2  10451  seqof2  14078  rlim2  15512  ello1mpt  15537  o1compt  15603  sumfc  15725  fsum  15736  fsumf1o  15739  sumss  15740  fsumcvg2  15743  fsumadd  15756  isummulc2  15778  fsummulc2  15800  fsumrelem  15823  isumshft  15855  zprod  15953  fprod  15957  prodfc  15961  fprodf1o  15962  fprodmul  15976  fproddiv  15977  iserodd  16855  prdsbas3  17495  prdsdsval2  17498  invfuc  17990  yonedalem4b  18288  gsumdixp  20279  evlslem4  22034  elptr2  23512  ptunimpt  23533  ptcldmpt  23552  ptclsg  23553  txcnp  23558  ptcnplem  23559  cnmpt1t  23603  cnmptk2  23624  flfcnp2  23945  voliun  25507  mbfeqalem1  25594  mbfpos  25604  mbfposb  25606  mbfsup  25617  mbfinf  25618  mbflim  25621  i1fposd  25660  isibl2  25719  itgmpt  25736  itgeqa  25767  itggt0  25797  itgcn  25798  limcmpt  25836  lhop2  25972  itgsubstlem  26007  itgsubst  26008  elplyd  26159  coeeq2  26199  dgrle  26200  ulmss  26358  itgulm2  26370  leibpi  26904  rlimcnp  26927  o1cxp  26937  lgamgulmlem2  26992  lgamgulmlem6  26996  fmptcof2  32635  itggt0cn  37714  elrfirn2  42719  eq0rabdioph  42799  monotoddzz  42967  aomclem8  43085  fmuldfeq  45612  vonioo  46711