Theorem fmpttd 5866

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   e. wcel 2209   |-> cmpt 4193   -->wf 5376

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4251  ax-pow 4313  ax-pr 4348

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-rab 2537  df-v 2823  df-sbc 3052  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4132  df-opab 4194  df-mpt 4195  df-id 4440  df-xp 4782  df-rel 4783  df-cnv 4784  df-co 4785  df-dm 4786  df-rn 4787  df-res 4788  df-ima 4789  df-iota 5340  df-fun 5382  df-fn 5383  df-f 5384  df-fv 5388

This theorem is used by:  fmpt3d  5867  pw2f1odclem  7140  mapxpen  7154  2omap  7324  ctmlemr  7454  ctssdclemn0  7456  ctssdc  7459  infnninf  7470  nnnninf  7472  ismkvnex  7501  seqf1og  10978  ccatcl  11382  swrdclg  11443  swrdwrdsymbg  11457  fsumf1o  12181  isumss  12182  fisumss  12183  fsumcl2lem  12189  fsumadd  12197  isumclim3  12214  isummulc2  12217  fsummulc2  12239  isumshft  12281  prodfdivap  12338  fprodf1o  12379  prodssdc  12380  fprodssdc  12381  fprodmul  12382  gzsumconst  14232  gzsummhm2  14235  gsumsncmn  14245  gsumzfi  14247  gsummptfidmadd  14250  gsummptfidmsplit  14253  gsummhm2fi  14264  gsumconstcmn  14265  gsum2dfilem1  14270  gsum2dfilem2  14271  gsum2dfi  14272  srglmhm  14403  srgrmhm  14404  ringlghm  14472  ringrghm  14473  gsumfsum  15031  expghmap  15050  snifpsrbagfi  15168  fczpsrbag  15169  psrass1filem  15186  rhmpsrfilem2  15194  psrmulvalfi  15197  psrmulclfilem  15198  psrlidmfi  15208  psrridmfi  15209  mvrffi  15218  mvrclfi  15226  tgrest  15412  resttopon  15414  rest0  15422  cnpfval  15438  txcnp  15514  uptx  15517  cnmpt11  15526  bdxmet  15744  cncfmptc  15839  cncfmptid  15840  cdivcncfap  15847  mulcncf  15851  maxcncf  15858  mincncf  15859  ivthreinc  15888  hovercncf  15889  limcmpted  15906  dvfgg  15931  dvcnp2cntop  15942  dvmulxxbr  15945  dvcjbr  15951  dvexp  15954  dvrecap  15956  dvmptclx  15961  dvmptaddx  15962  dvmptmulx  15963  dvmptcjx  15967  dvef  15970  elply2  15978  plyf  15980  elplyd  15984  dvply2g  16009  lgseisenlem3  16413  lgseisenlem4  16414  incistruhgr  16553  pw1map  17247  subctctexmid  17252  nninffeq  17286  iswomni0  17325  dceqnconst  17334  dcapnconst  17335