Theorem fmpt3d 7062

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 7061	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶)
3		fmpt3d.1	. . 3 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵))
4	3	feq1d 6644	. 2 ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶))
5	2, 4	mpbird 257	1 ⊢ (𝜑 → 𝐹:𝐴⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114   ↦ cmpt 5167  ⟶wf 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-fun 6494  df-fn 6495  df-f 6496

This theorem is referenced by:  fmptco  7076  off  7642  caofinvl  7656  curry1f  8049  curry2f  8051  fseqenlem1  9937  indf  12156  pfxf  14634  rpnnen2lem2  16173  1arithlem3  16887  homaf  17988  funcestrcsetclem3  18099  funcsetcestrclem3  18113  prfcl  18160  curf1cl  18185  yonedainv  18238  vrmdf  18817  pmtrf  19421  psgnunilem5  19460  pj1f  19663  vrgpf  19734  gsummptfsadd  19890  gsummptfssub  19915  lspf  20960  uvcff  21781  subrgpsr  21966  mvrf  21973  mhpmulcl  22125  cpm2mf  22727  nmf2  24568  nmof  24694  cphnmf  25172  rrxcph  25369  uniioombllem2  25560  mbfi1fseqlem3  25694  itg2cnlem1  25738  dvmptco  25949  dvle  25984  taylpf  26342  ulmshftlem  26367  ulmshft  26368  ulmdvlem1  26378  psergf  26390  pserdvlem2  26406  logbf  26766  lmif  28867  vtxdgf  29555  brafn  32033  kbop  32039  off2  32729  ofoprabco  32752  tocycf  33193  sgnsf  33238  qqhf  34146  esumcocn  34240  ofcf  34263  mbfmcst  34419  dstrvprob  34632  dstfrvclim1  34638  signstf  34726  fsovfd  44457  dssmapnvod  44465  binomcxplemnotnn0  44801  sge0seq  46892  hoicvr  46994  hoicvrrex  47002