Theorem fmpttd 5832

Description: Version of fmptd 5831 with inlined definition. Domain and codomain of the mapping operation; deduction form. (Contributed by Glauco Siliprandi, 23-Oct-2021.) (Proof shortened by BJ, 16-Aug-2022.)

Hypothesis

Ref	Expression
fmpttd.1	|- ( ( ph /\ x e. A ) -> B e. C )

Assertion

Ref	Expression
fmpttd	|- ( ph -> ( x e. A |-> B ) : A --> C )

Distinct variable groups:   x, A   x, C   ph, x

Allowed substitution hint:   B( x)

Proof of Theorem fmpttd

Step	Hyp	Ref	Expression
1		fmpttd.1	. 2 |- ( ( ph /\ x e. A ) -> B e. C )
2		eqid 2232	. 2 |- ( x e. A |-> B ) = ( x e. A |-> B )
3	1, 2	fmptd 5831	1 |- ( ph -> ( x e. A |-> B ) : A --> C )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2203   |-> cmpt 4171   -->wf 5348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2206  ax-ext 2214  ax-sep 4228  ax-pow 4287  ax-pr 4322

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-rab 2529  df-v 2815  df-sbc 3043  df-un 3215  df-in 3217  df-ss 3224  df-pw 3671  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-br 4110  df-opab 4172  df-mpt 4173  df-id 4414  df-xp 4755  df-rel 4756  df-cnv 4757  df-co 4758  df-dm 4759  df-rn 4760  df-res 4761  df-ima 4762  df-iota 5312  df-fun 5354  df-fn 5355  df-f 5356  df-fv 5360

This theorem is referenced by:  fmpt3d  5833  pw2f1odclem  7087  mapxpen  7101  2omap  7269  ctmlemr  7399  ctssdclemn0  7401  ctssdc  7404  infnninf  7415  nnnninf  7417  ismkvnex  7446  seqf1og  10883  ccatcl  11281  swrdclg  11342  swrdwrdsymbg  11356  fsumf1o  12076  isumss  12077  fisumss  12078  fsumcl2lem  12084  fsumadd  12092  isumclim3  12109  isummulc2  12112  fsummulc2  12134  isumshft  12176  prodfdivap  12233  fprodf1o  12274  prodssdc  12275  fprodssdc  12276  fprodmul  12277  gsumfzz  13708  gsumfzmptfidmadd  14056  gsumfzconst  14058  gsumfzmhm2  14061  srglmhm  14137  srgrmhm  14138  ringlghm  14205  ringrghm  14206  gsumfzfsumlemm  14735  expghmap  14755  fczpsrbag  14820  mplsubgfilemm  14853  tgrest  15034  resttopon  15036  rest0  15044  cnpfval  15060  txcnp  15136  uptx  15139  cnmpt11  15148  bdxmet  15366  cncfmptc  15461  cncfmptid  15462  cdivcncfap  15469  mulcncf  15473  maxcncf  15480  mincncf  15481  ivthreinc  15510  hovercncf  15511  limcmpted  15528  dvfgg  15553  dvcnp2cntop  15564  dvmulxxbr  15567  dvcjbr  15573  dvexp  15576  dvrecap  15578  dvmptclx  15583  dvmptaddx  15584  dvmptmulx  15585  dvmptcjx  15589  dvef  15592  elply2  15600  plyf  15602  elplyd  15606  dvply2g  15631  lgseisenlem3  15945  lgseisenlem4  15946  incistruhgr  16085  pw1map  16769  subctctexmid  16774  nninffeq  16798  iswomni0  16836  dceqnconst  16846  dcapnconst  16847  gfsumsn  16867  gfsumz  16869