Theorem fmpt3d 7113

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143   ↦ cmpt 5193  ⟶wf 6534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-fun 6540  df-fn 6541  df-f 6542

This theorem is referenced by:  fmptco  7127  off  7694  caofinvl  7708  curry1f  8102  curry2f  8104  fseqenlem1  10009  indf  12225  pfxf  14720  rpnnen2lem2  16272  1arithlem3  16986  homaf  18088  funcestrcsetclem3  18199  funcsetcestrclem3  18213  prfcl  18260  curf1cl  18285  yonedainv  18338  vrmdf  18918  pmtrf  19526  psgnunilem5  19565  pj1f  19768  vrgpf  19839  gsummptfsadd  19995  gsummptfssub  20020  lspf  21076  uvcff  21922  subrgpsr  22108  mvrf  22115  mhpmulcl  22293  cpm2mf  22890  nmf2  24731  nmof  24857  cphnmf  25335  rrxcph  25532  uniioombllem2  25723  mbfi1fseqlem3  25857  itg2cnlem1  25901  dvmptco  26112  dvle  26147  taylpf  26510  ulmshftlem  26533  ulmshft  26534  ulmdvlem1  26544  psergf  26556  pserdvlem2  26572  logbf  26935  lmif  29075  vtxdgf  29802  brafn  32280  kbop  32286  off2  32967  ofoprabco  32990  tocycf  33418  sgnsf  33463  mplasclco  33887  qqhf  34357  esumcocn  34451  ofcf  34474  mbfmcst  34630  dstrvprob  34843  dstfrvclim1  34849  signstf  34934  fsovfd  44721  dssmapnvod  44729  binomcxplemnotnn0  45049  sge0seq  47143  hoicvr  47245  hoicvrrex  47253