Theorem fmpttd 5748

Description: Version of fmptd 5747 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 2206	. 2 |- ( x e. A |-> B ) = ( x e. A |-> B )
3	1, 2	fmptd 5747	1 |- ( ph -> ( x e. A |-> B ) : A --> C )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2177   |-> cmpt 4113   -->wf 5276

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-14 2180  ax-ext 2188  ax-sep 4170  ax-pow 4226  ax-pr 4261

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-rex 2491  df-rab 2494  df-v 2775  df-sbc 3003  df-un 3174  df-in 3176  df-ss 3183  df-pw 3623  df-sn 3644  df-pr 3645  df-op 3647  df-uni 3857  df-br 4052  df-opab 4114  df-mpt 4115  df-id 4348  df-xp 4689  df-rel 4690  df-cnv 4691  df-co 4692  df-dm 4693  df-rn 4694  df-res 4695  df-ima 4696  df-iota 5241  df-fun 5282  df-fn 5283  df-f 5284  df-fv 5288

This theorem is referenced by:  fmpt3d  5749  pw2f1odclem  6946  ctmlemr  7225  ctssdclemn0  7227  ctssdc  7230  infnninf  7241  nnnninf  7243  ismkvnex  7272  seqf1og  10688  ccatcl  11072  swrdclg  11126  swrdwrdsymbg  11140  fsumf1o  11776  isumss  11777  fisumss  11778  fsumcl2lem  11784  fsumadd  11792  isumclim3  11809  isummulc2  11812  fsummulc2  11834  isumshft  11876  prodfdivap  11933  fprodf1o  11974  prodssdc  11975  fprodssdc  11976  fprodmul  11977  gsumfzz  13402  gsumfzmptfidmadd  13750  gsumfzconst  13752  gsumfzmhm2  13755  srglmhm  13830  srgrmhm  13831  ringlghm  13898  ringrghm  13899  gsumfzfsumlemm  14424  expghmap  14444  fczpsrbag  14508  mplsubgfilemm  14535  tgrest  14716  resttopon  14718  rest0  14726  cnpfval  14742  txcnp  14818  uptx  14821  cnmpt11  14830  bdxmet  15048  cncfmptc  15143  cncfmptid  15144  cdivcncfap  15151  mulcncf  15155  maxcncf  15162  mincncf  15163  ivthreinc  15192  hovercncf  15193  limcmpted  15210  dvfgg  15235  dvcnp2cntop  15246  dvmulxxbr  15249  dvcjbr  15255  dvexp  15258  dvrecap  15260  dvmptclx  15265  dvmptaddx  15266  dvmptmulx  15267  dvmptcjx  15271  dvef  15274  elply2  15282  plyf  15284  elplyd  15288  dvply2g  15313  lgseisenlem3  15624  lgseisenlem4  15625  incistruhgr  15761  2omap  16071  pw1map  16073  subctctexmid  16078  nninffeq  16098  iswomni0  16131  dceqnconst  16140  dcapnconst  16141