Theorem fmpt3d 7135

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1536   ∈ wcel 2105   ↦ cmpt 5230  ⟶wf 6558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-fun 6564  df-fn 6565  df-f 6566

This theorem is referenced by:  fmptco  7148  off  7714  caofinvl  7728  curry1f  8129  curry2f  8131  fseqenlem1  10061  pfxf  14714  rpnnen2lem2  16247  1arithlem3  16958  homaf  18083  funcestrcsetclem3  18197  funcsetcestrclem3  18211  prfcl  18258  curf1cl  18284  yonedainv  18337  vrmdf  18883  pmtrf  19487  psgnunilem5  19526  pj1f  19729  vrgpf  19800  gsummptfsadd  19956  gsummptfssub  19981  lspf  20989  uvcff  21828  subrgpsr  22015  mvrf  22022  mhpmulcl  22170  cpm2mf  22773  nmf2  24621  nmof  24755  cphnmf  25242  rrxcph  25439  uniioombllem2  25631  mbfi1fseqlem3  25766  itg2cnlem1  25810  dvmptco  26024  dvle  26060  taylpf  26421  ulmshftlem  26446  ulmshft  26447  ulmdvlem1  26457  psergf  26469  pserdvlem2  26486  logbf  26846  lmif  28807  vtxdgf  29503  brafn  31975  kbop  31981  off2  32657  ofoprabco  32680  tocycf  33119  sgnsf  33164  qqhf  33948  indf  33995  esumcocn  34060  ofcf  34083  mbfmcst  34240  dstrvprob  34452  dstfrvclim1  34458  signstf  34559  fsovfd  44001  dssmapnvod  44009  binomcxplemnotnn0  44351  sge0seq  46401  hoicvrrex  46511