Theorem nffvmpt1 6872

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

Syntax hints:  Ⅎwnfc 2877   ↦ cmpt 5191  ‘cfv 6514

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-iota 6467  df-fv 6522

This theorem is referenced by:  fvmptt  6991  fmptco  7104  offval2f  7671  offval2  7676  ofrfval2  7677  mptelixpg  8911  dom2lem  8966  cantnflem1  9649  acni2  10006  axcc2  10397  seqof2  14032  rlim2  15469  ello1mpt  15494  o1compt  15560  sumfc  15682  fsum  15693  fsumf1o  15696  sumss  15697  fsumcvg2  15700  fsumadd  15713  isummulc2  15735  fsummulc2  15757  fsumrelem  15780  isumshft  15812  zprod  15910  fprod  15914  prodfc  15918  fprodf1o  15919  fprodmul  15933  fproddiv  15934  iserodd  16813  prdsbas3  17451  prdsdsval2  17454  invfuc  17946  yonedalem4b  18244  gsumdixp  20235  evlslem4  21990  elptr2  23468  ptunimpt  23489  ptcldmpt  23508  ptclsg  23509  txcnp  23514  ptcnplem  23515  cnmpt1t  23559  cnmptk2  23580  flfcnp2  23901  voliun  25462  mbfeqalem1  25549  mbfpos  25559  mbfposb  25561  mbfsup  25572  mbfinf  25573  mbflim  25576  i1fposd  25615  isibl2  25674  itgmpt  25691  itgeqa  25722  itggt0  25752  itgcn  25753  limcmpt  25791  lhop2  25927  itgsubstlem  25962  itgsubst  25963  elplyd  26114  coeeq2  26154  dgrle  26155  ulmss  26313  itgulm2  26325  leibpi  26859  rlimcnp  26882  o1cxp  26892  lgamgulmlem2  26947  lgamgulmlem6  26951  fmptcof2  32588  itggt0cn  37691  elrfirn2  42691  eq0rabdioph  42771  monotoddzz  42939  aomclem8  43057  fmuldfeq  45588  vonioo  46687