Theorem fmpt3d 7070

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

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

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 5243  ax-pr 5379

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-fun 6502  df-fn 6503  df-f 6504

This theorem is referenced by:  fmptco  7084  off  7650  caofinvl  7664  curry1f  8058  curry2f  8060  fseqenlem1  9946  pfxf  14616  rpnnen2lem2  16152  1arithlem3  16865  homaf  17966  funcestrcsetclem3  18077  funcsetcestrclem3  18091  prfcl  18138  curf1cl  18163  yonedainv  18216  vrmdf  18795  pmtrf  19396  psgnunilem5  19435  pj1f  19638  vrgpf  19709  gsummptfsadd  19865  gsummptfssub  19890  lspf  20937  uvcff  21758  subrgpsr  21945  mvrf  21952  mhpmulcl  22104  cpm2mf  22708  nmf2  24549  nmof  24675  cphnmf  25163  rrxcph  25360  uniioombllem2  25552  mbfi1fseqlem3  25686  itg2cnlem1  25730  dvmptco  25944  dvle  25980  taylpf  26341  ulmshftlem  26366  ulmshft  26367  ulmdvlem1  26377  psergf  26389  pserdvlem2  26406  logbf  26767  lmif  28869  vtxdgf  29557  brafn  32034  kbop  32040  off2  32730  ofoprabco  32753  indf  32944  tocycf  33210  sgnsf  33255  qqhf  34163  esumcocn  34257  ofcf  34280  mbfmcst  34436  dstrvprob  34649  dstfrvclim1  34655  signstf  34743  fsovfd  44365  dssmapnvod  44373  binomcxplemnotnn0  44709  sge0seq  46801  hoicvrrex  46911