Theorem fmpt3d 6990

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ∈ wcel 2106   ↦ cmpt 5157  ⟶wf 6429

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-fun 6435  df-fn 6436  df-f 6437

This theorem is referenced by:  fmptco  7001  off  7551  caofinvl  7563  curry1f  7946  curry2f  7948  fseqenlem1  9780  pfxf  14393  rpnnen2lem2  15924  1arithlem3  16626  homaf  17745  funcestrcsetclem3  17859  funcsetcestrclem3  17873  prfcl  17920  curf1cl  17946  yonedainv  17999  vrmdf  18497  pmtrf  19063  psgnunilem5  19102  pj1f  19303  vrgpf  19374  gsummptfsadd  19525  gsummptfssub  19550  lspf  20236  uvcff  20998  subrgpsr  21188  mvrf  21193  mhpmulcl  21339  cpm2mf  21901  nmf2  23749  nmof  23883  cphnmf  24359  rrxcph  24556  uniioombllem2  24747  mbfi1fseqlem3  24882  itg2cnlem1  24926  dvmptco  25136  dvle  25171  taylpf  25525  ulmshftlem  25548  ulmshft  25549  ulmdvlem1  25559  psergf  25571  pserdvlem2  25587  logbf  25939  lmif  27146  vtxdgf  27838  brafn  30309  kbop  30315  off2  30978  ofoprabco  31001  tocycf  31384  sgnsf  31429  qqhf  31936  indf  31983  esumcocn  32048  ofcf  32071  mbfmcst  32226  dstrvprob  32438  dstfrvclim1  32444  signstf  32545  fsovfd  41620  dssmapnvod  41628  binomcxplemnotnn0  41974  sge0seq  43984  hoicvrrex  44094