Theorem fmpt3d 7054

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ↦ cmpt 5176  ⟶wf 6482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  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 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-fun 6488  df-fn 6489  df-f 6490

This theorem is referenced by:  fmptco  7067  off  7635  caofinvl  7649  curry1f  8046  curry2f  8048  fseqenlem1  9937  pfxf  14605  rpnnen2lem2  16142  1arithlem3  16855  homaf  17955  funcestrcsetclem3  18066  funcsetcestrclem3  18080  prfcl  18127  curf1cl  18152  yonedainv  18205  vrmdf  18750  pmtrf  19352  psgnunilem5  19391  pj1f  19594  vrgpf  19665  gsummptfsadd  19821  gsummptfssub  19846  lspf  20895  uvcff  21716  subrgpsr  21903  mvrf  21910  mhpmulcl  22052  cpm2mf  22655  nmf2  24497  nmof  24623  cphnmf  25111  rrxcph  25308  uniioombllem2  25500  mbfi1fseqlem3  25634  itg2cnlem1  25678  dvmptco  25892  dvle  25928  taylpf  26289  ulmshftlem  26314  ulmshft  26315  ulmdvlem1  26325  psergf  26337  pserdvlem2  26354  logbf  26715  lmif  28748  vtxdgf  29435  brafn  31909  kbop  31915  off2  32598  ofoprabco  32621  indf  32811  tocycf  33072  sgnsf  33117  qqhf  33955  esumcocn  34049  ofcf  34072  mbfmcst  34229  dstrvprob  34442  dstfrvclim1  34448  signstf  34536  fsovfd  43988  dssmapnvod  43996  binomcxplemnotnn0  44332  sge0seq  46431  hoicvrrex  46541