Theorem fmpt3d 7064

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119   ↦ cmpt 5160  ⟶wf 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-fun 6494  df-fn 6495  df-f 6496

This theorem is referenced by:  fmptco  7078  off  7645  caofinvl  7659  curry1f  8052  curry2f  8054  fseqenlem1  9944  indf  12163  pfxf  14641  rpnnen2lem2  16180  1arithlem3  16894  homaf  17995  funcestrcsetclem3  18106  funcsetcestrclem3  18120  prfcl  18167  curf1cl  18192  yonedainv  18245  vrmdf  18824  pmtrf  19428  psgnunilem5  19467  pj1f  19670  vrgpf  19741  gsummptfsadd  19897  gsummptfssub  19922  lspf  20971  uvcff  21773  subrgpsr  21959  mvrf  21966  mhpmulcl  22144  cpm2mf  22742  nmf2  24583  nmof  24709  cphnmf  25187  rrxcph  25384  uniioombllem2  25575  mbfi1fseqlem3  25709  itg2cnlem1  25753  dvmptco  25964  dvle  25999  taylpf  26356  ulmshftlem  26379  ulmshft  26380  ulmdvlem1  26390  psergf  26402  pserdvlem2  26418  logbf  26778  lmif  28878  vtxdgf  29565  brafn  32043  kbop  32049  off2  32740  ofoprabco  32763  tocycf  33205  sgnsf  33250  mplasclco  33707  qqhf  34177  esumcocn  34271  ofcf  34294  mbfmcst  34450  dstrvprob  34663  dstfrvclim1  34669  signstf  34757  fsovfd  44463  dssmapnvod  44471  binomcxplemnotnn0  44807  sge0seq  46896  hoicvr  46998  hoicvrrex  47006