Theorem fmpt3d 6972

Description: Domain and codomain of the mapping operation; deduction form. (Contributed by Thierry Arnoux, 4-Jun-2017.)

Hypotheses

Ref	Expression
fmpt3d.1	⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵))
fmpt3d.2	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)

Assertion

Ref	Expression
fmpt3d	⊢ (𝜑 → 𝐹:𝐴⟶𝐶)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐶   𝜑,𝑥

Allowed substitution hints:   𝐵(𝑥)   𝐹(𝑥)

Proof of Theorem fmpt3d

Step	Hyp	Ref	Expression
1		fmpt3d.2	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)
2	1	fmpttd 6971	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶)
3		fmpt3d.1	. . 3 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵))
4	3	feq1d 6569	. 2 ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶))
5	2, 4	mpbird 256	1 ⊢ (𝜑 → 𝐹:𝐴⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2108   ↦ cmpt 5153  ⟶wf 6414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-fun 6420  df-fn 6421  df-f 6422

This theorem is referenced by:  fmptco  6983  off  7529  caofinvl  7541  curry1f  7917  curry2f  7919  fseqenlem1  9711  pfxf  14321  rpnnen2lem2  15852  1arithlem3  16554  homaf  17661  funcestrcsetclem3  17775  funcsetcestrclem3  17789  prfcl  17836  curf1cl  17862  yonedainv  17915  vrmdf  18412  pmtrf  18978  psgnunilem5  19017  pj1f  19218  vrgpf  19289  gsummptfsadd  19440  gsummptfssub  19465  lspf  20151  uvcff  20908  subrgpsr  21098  mvrf  21103  mhpmulcl  21249  cpm2mf  21809  nmf2  23655  nmof  23789  cphnmf  24264  rrxcph  24461  uniioombllem2  24652  mbfi1fseqlem3  24787  itg2cnlem1  24831  dvmptco  25041  dvle  25076  taylpf  25430  ulmshftlem  25453  ulmshft  25454  ulmdvlem1  25464  psergf  25476  pserdvlem2  25492  logbf  25844  lmif  27050  vtxdgf  27741  brafn  30210  kbop  30216  off2  30879  ofoprabco  30903  tocycf  31286  sgnsf  31331  qqhf  31836  indf  31883  esumcocn  31948  ofcf  31971  mbfmcst  32126  dstrvprob  32338  dstfrvclim1  32344  signstf  32445  fsovfd  41509  dssmapnvod  41517  binomcxplemnotnn0  41863  sge0seq  43874  hoicvrrex  43984