Theorem fmpt3d 7058

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113   ↦ cmpt 5176  ⟶wf 6485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-fun 6491  df-fn 6492  df-f 6493

This theorem is referenced by:  fmptco  7071  off  7637  caofinvl  7651  curry1f  8045  curry2f  8047  fseqenlem1  9926  pfxf  14595  rpnnen2lem2  16131  1arithlem3  16844  homaf  17945  funcestrcsetclem3  18056  funcsetcestrclem3  18070  prfcl  18117  curf1cl  18142  yonedainv  18195  vrmdf  18774  pmtrf  19375  psgnunilem5  19414  pj1f  19617  vrgpf  19688  gsummptfsadd  19844  gsummptfssub  19869  lspf  20916  uvcff  21737  subrgpsr  21924  mvrf  21931  mhpmulcl  22083  cpm2mf  22687  nmf2  24528  nmof  24654  cphnmf  25142  rrxcph  25339  uniioombllem2  25531  mbfi1fseqlem3  25665  itg2cnlem1  25709  dvmptco  25923  dvle  25959  taylpf  26320  ulmshftlem  26345  ulmshft  26346  ulmdvlem1  26356  psergf  26368  pserdvlem2  26385  logbf  26746  lmif  28783  vtxdgf  29471  brafn  31948  kbop  31954  off2  32645  ofoprabco  32668  indf  32862  tocycf  33127  sgnsf  33172  qqhf  34071  esumcocn  34165  ofcf  34188  mbfmcst  34344  dstrvprob  34557  dstfrvclim1  34563  signstf  34651  fsovfd  44169  dssmapnvod  44177  binomcxplemnotnn0  44513  sge0seq  46606  hoicvrrex  46716