Theorem nffvmpt1 6111

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

Syntax hints:  Ⅎwnfc 2738   ↦ cmpt 4643  ‘cfv 5804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-iota 5768  df-fv 5812

This theorem is referenced by:  fvmptt  6208  fmptco  6303  offval2f  6807  offval2  6812  ofrfval2  6813  mptelixpg  7831  dom2lem  7881  cantnflem1  8469  acni2  8752  axcc2  9142  seqof2  12721  rlim2  14075  ello1mpt  14100  o1compt  14166  sumfc  14287  fsum  14298  fsumf1o  14301  sumss  14302  fsumcvg2  14305  fsumadd  14317  isummulc2  14335  fsummulc2  14358  fsumrelem  14380  isumshft  14410  zprod  14506  fprod  14510  prodfc  14514  fprodf1o  14515  fprodmul  14529  fproddiv  14530  iserodd  15378  prdsbas3  15964  prdsdsval2  15967  invfuc  16457  yonedalem4b  16739  gsumdixp  18432  evlslem4  19329  elptr2  21187  ptunimpt  21208  ptcldmpt  21227  ptclsg  21228  txcnp  21233  ptcnplem  21234  cnmpt1t  21278  cnmptk2  21299  flfcnp2  21621  voliun  23129  mbfeqalem  23215  mbfpos  23224  mbfposb  23226  mbfsup  23237  mbfinf  23238  mbflim  23241  i1fposd  23280  isibl2  23339  itgmpt  23355  itgeqa  23386  itggt0  23414  itgcn  23415  limcmpt  23453  lhop2  23582  itgsubstlem  23615  itgsubst  23616  elplyd  23762  coeeq2  23802  dgrle  23803  ulmss  23955  itgulm2  23967  leibpi  24469  rlimcnp  24492  o1cxp  24501  lgamgulmlem2  24556  lgamgulmlem6  24560  fmptcof2  28839  itggt0cn  32652  elrfirn2  36277  eq0rabdioph  36358  monotoddzz  36526  aomclem8  36649  fmuldfeq  38650  vonioo  39573