Theorem fmpt3d 7092

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1559   ∈ wcel 2141   ↦ cmpt 5178  ⟶wf 6512

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-pr 5387

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5538  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-fun 6518  df-fn 6519  df-f 6520

This theorem is referenced by:  fmptco  7106  off  7673  caofinvl  7687  curry1f  8079  curry2f  8081  fseqenlem1  9974  indf  12195  pfxf  14688  rpnnen2lem2  16238  1arithlem3  16952  homaf  18054  funcestrcsetclem3  18165  funcsetcestrclem3  18179  prfcl  18226  curf1cl  18251  yonedainv  18304  vrmdf  18883  pmtrf  19486  psgnunilem5  19525  pj1f  19728  vrgpf  19799  gsummptfsadd  19955  gsummptfssub  19980  lspf  21029  uvcff  21831  subrgpsr  22017  mvrf  22024  mhpmulcl  22202  cpm2mf  22800  nmf2  24641  nmof  24767  cphnmf  25245  rrxcph  25442  uniioombllem2  25633  mbfi1fseqlem3  25767  itg2cnlem1  25811  dvmptco  26022  dvle  26057  taylpf  26417  ulmshftlem  26440  ulmshft  26441  ulmdvlem1  26451  psergf  26463  pserdvlem2  26479  logbf  26842  lmif  28942  vtxdgf  29629  brafn  32107  kbop  32113  off2  32804  ofoprabco  32827  tocycf  33258  sgnsf  33303  mplasclco  33774  qqhf  34244  esumcocn  34338  ofcf  34361  mbfmcst  34517  dstrvprob  34730  dstfrvclim1  34736  signstf  34821  fsovfd  44549  dssmapnvod  44557  binomcxplemnotnn0  44893  sge0seq  46981  hoicvr  47083  hoicvrrex  47091