Theorem nffvmpt1 6199

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

Syntax hints:  Ⅎwnfc 2751   ↦ cmpt 4729  ‘cfv 5888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-iota 5851  df-fv 5896

This theorem is referenced by:  fvmptt  6300  fmptco  6396  offval2f  6909  offval2  6914  ofrfval2  6915  mptelixpg  7945  dom2lem  7995  cantnflem1  8586  acni2  8869  axcc2  9259  seqof2  12859  rlim2  14227  ello1mpt  14252  o1compt  14318  sumfc  14440  fsum  14451  fsumf1o  14454  sumss  14455  fsumcvg2  14458  fsumadd  14470  isummulc2  14493  fsummulc2  14516  fsumrelem  14539  isumshft  14571  zprod  14667  fprod  14671  prodfc  14675  fprodf1o  14676  fprodmul  14690  fproddiv  14691  iserodd  15540  prdsbas3  16141  prdsdsval2  16144  invfuc  16634  yonedalem4b  16916  gsumdixp  18609  evlslem4  19508  elptr2  21377  ptunimpt  21398  ptcldmpt  21417  ptclsg  21418  txcnp  21423  ptcnplem  21424  cnmpt1t  21468  cnmptk2  21489  flfcnp2  21811  voliun  23322  mbfeqalem  23409  mbfpos  23418  mbfposb  23420  mbfsup  23431  mbfinf  23432  mbflim  23435  i1fposd  23474  isibl2  23533  itgmpt  23549  itgeqa  23580  itggt0  23608  itgcn  23609  limcmpt  23647  lhop2  23778  itgsubstlem  23811  itgsubst  23812  elplyd  23958  coeeq2  23998  dgrle  23999  ulmss  24151  itgulm2  24163  leibpi  24669  rlimcnp  24692  o1cxp  24701  lgamgulmlem2  24756  lgamgulmlem6  24760  fmptcof2  29457  itggt0cn  33482  elrfirn2  37259  eq0rabdioph  37340  monotoddzz  37508  aomclem8  37631  fmuldfeq  39815  vonioo  40896