Theorem fmpt3d 7109

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567   ∈ wcel 2149   ↦ cmpt 5193  ⟶wf 6529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-pr 5402

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-fun 6535  df-fn 6536  df-f 6537

This theorem is referenced by:  fmptco  7123  off  7690  caofinvl  7704  curry1f  8097  curry2f  8099  fseqenlem1  10004  indf  12220  pfxf  14714  rpnnen2lem2  16267  1arithlem3  16981  homaf  18083  funcestrcsetclem3  18194  funcsetcestrclem3  18208  prfcl  18255  curf1cl  18280  yonedainv  18333  vrmdf  18913  pmtrf  19521  psgnunilem5  19560  pj1f  19763  vrgpf  19834  gsummptfsadd  19990  gsummptfssub  20015  lspf  21069  uvcff  21906  subrgpsr  22092  mvrf  22099  mhpmulcl  22277  cpm2mf  22874  nmf2  24715  nmof  24841  cphnmf  25319  rrxcph  25516  uniioombllem2  25707  mbfi1fseqlem3  25841  itg2cnlem1  25885  dvmptco  26096  dvle  26131  taylpf  26491  ulmshftlem  26514  ulmshft  26515  ulmdvlem1  26525  psergf  26537  pserdvlem2  26553  logbf  26916  lmif  29048  vtxdgf  29758  brafn  32236  kbop  32242  off2  32923  ofoprabco  32946  tocycf  33374  sgnsf  33419  mplasclco  33847  qqhf  34317  esumcocn  34411  ofcf  34434  mbfmcst  34590  dstrvprob  34803  dstfrvclim1  34809  signstf  34894  fsovfd  44623  dssmapnvod  44631  binomcxplemnotnn0  44951  sge0seq  47045  hoicvr  47147  hoicvrrex  47155