Theorem fmpt3d 6857

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111   ↦ cmpt 5110  ⟶wf 6320

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-fv 6332

This theorem is referenced by:  fmptco  6868  off  7404  caofinvl  7416  curry1f  7784  curry2f  7786  fseqenlem1  9435  pfxf  14033  rpnnen2lem2  15560  1arithlem3  16251  homaf  17282  funcestrcsetclem3  17384  funcsetcestrclem3  17398  prfcl  17445  curf1cl  17470  yonedainv  17523  vrmdf  18015  pmtrf  18575  psgnunilem5  18614  pj1f  18815  vrgpf  18886  gsummptfsadd  19037  gsummptfssub  19062  lspf  19739  uvcff  20480  subrgpsr  20657  mvrf  20662  cpm2mf  21357  nmf2  23199  nmof  23325  cphnmf  23800  rrxcph  23996  uniioombllem2  24187  mbfi1fseqlem3  24321  itg2cnlem1  24365  dvmptco  24575  dvle  24610  taylpf  24961  ulmshftlem  24984  ulmshft  24985  ulmdvlem1  24995  psergf  25007  pserdvlem2  25023  logbf  25375  lmif  26579  vtxdgf  27261  brafn  29730  kbop  29736  off2  30402  ofoprabco  30427  tocycf  30809  sgnsf  30854  qqhf  31337  indf  31384  esumcocn  31449  ofcf  31472  mbfmcst  31627  dstrvprob  31839  dstfrvclim1  31845  signstf  31946  fsovfd  40713  dssmapnvod  40721  binomcxplemnotnn0  41060  sge0seq  43085  hoicvrrex  43195