Theorem nffvmpt1 6828

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

Syntax hints:  Ⅎwnfc 2879   ↦ cmpt 5167  ‘cfv 6476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-br 5087  df-opab 5149  df-mpt 5168  df-iota 6432  df-fv 6484

This theorem is referenced by:  fvmptt  6944  fmptco  7057  offval2f  7620  offval2  7625  ofrfval2  7626  mptelixpg  8854  dom2lem  8909  cantnflem1  9574  acni2  9932  axcc2  10323  seqof2  13962  rlim2  15398  ello1mpt  15423  o1compt  15489  sumfc  15611  fsum  15622  fsumf1o  15625  sumss  15626  fsumcvg2  15629  fsumadd  15642  isummulc2  15664  fsummulc2  15686  fsumrelem  15709  isumshft  15741  zprod  15839  fprod  15843  prodfc  15847  fprodf1o  15848  fprodmul  15862  fproddiv  15863  iserodd  16742  prdsbas3  17380  prdsdsval2  17383  invfuc  17879  yonedalem4b  18177  gsumdixp  20232  evlslem4  22006  elptr2  23484  ptunimpt  23505  ptcldmpt  23524  ptclsg  23525  txcnp  23530  ptcnplem  23531  cnmpt1t  23575  cnmptk2  23596  flfcnp2  23917  voliun  25477  mbfeqalem1  25564  mbfpos  25574  mbfposb  25576  mbfsup  25587  mbfinf  25588  mbflim  25591  i1fposd  25630  isibl2  25689  itgmpt  25706  itgeqa  25737  itggt0  25767  itgcn  25768  limcmpt  25806  lhop2  25942  itgsubstlem  25977  itgsubst  25978  elplyd  26129  coeeq2  26169  dgrle  26170  ulmss  26328  itgulm2  26340  leibpi  26874  rlimcnp  26897  o1cxp  26907  lgamgulmlem2  26962  lgamgulmlem6  26966  fmptcof2  32631  itggt0cn  37730  elrfirn2  42729  eq0rabdioph  42809  monotoddzz  42976  aomclem8  43094  fmuldfeq  45623  vonioo  46720