Theorem fmpt3d 7115

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106   ↦ cmpt 5231  ⟶wf 6539

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-fun 6545  df-fn 6546  df-f 6547

This theorem is referenced by:  fmptco  7126  off  7687  caofinvl  7699  curry1f  8091  curry2f  8093  fseqenlem1  10018  pfxf  14629  rpnnen2lem2  16157  1arithlem3  16857  homaf  17979  funcestrcsetclem3  18093  funcsetcestrclem3  18107  prfcl  18154  curf1cl  18180  yonedainv  18233  vrmdf  18738  pmtrf  19322  psgnunilem5  19361  pj1f  19564  vrgpf  19635  gsummptfsadd  19791  gsummptfssub  19816  lspf  20584  uvcff  21345  subrgpsr  21538  mvrf  21543  mhpmulcl  21691  cpm2mf  22253  nmf2  24101  nmof  24235  cphnmf  24711  rrxcph  24908  uniioombllem2  25099  mbfi1fseqlem3  25234  itg2cnlem1  25278  dvmptco  25488  dvle  25523  taylpf  25877  ulmshftlem  25900  ulmshft  25901  ulmdvlem1  25911  psergf  25923  pserdvlem2  25939  logbf  26291  lmif  28033  vtxdgf  28725  brafn  31195  kbop  31201  off2  31861  ofoprabco  31884  tocycf  32271  sgnsf  32316  qqhf  32961  indf  33008  esumcocn  33073  ofcf  33096  mbfmcst  33253  dstrvprob  33465  dstfrvclim1  33471  signstf  33572  fsovfd  42753  dssmapnvod  42761  binomcxplemnotnn0  43105  sge0seq  45152  hoicvrrex  45262