Theorem fmpt3d 7091

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ↦ cmpt 5191  ⟶wf 6510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-fun 6516  df-fn 6517  df-f 6518

This theorem is referenced by:  fmptco  7104  off  7674  caofinvl  7688  curry1f  8088  curry2f  8090  fseqenlem1  9984  pfxf  14652  rpnnen2lem2  16190  1arithlem3  16903  homaf  17999  funcestrcsetclem3  18110  funcsetcestrclem3  18124  prfcl  18171  curf1cl  18196  yonedainv  18249  vrmdf  18792  pmtrf  19392  psgnunilem5  19431  pj1f  19634  vrgpf  19705  gsummptfsadd  19861  gsummptfssub  19886  lspf  20887  uvcff  21707  subrgpsr  21894  mvrf  21901  mhpmulcl  22043  cpm2mf  22646  nmf2  24488  nmof  24614  cphnmf  25102  rrxcph  25299  uniioombllem2  25491  mbfi1fseqlem3  25625  itg2cnlem1  25669  dvmptco  25883  dvle  25919  taylpf  26280  ulmshftlem  26305  ulmshft  26306  ulmdvlem1  26316  psergf  26328  pserdvlem2  26345  logbf  26706  lmif  28719  vtxdgf  29406  brafn  31883  kbop  31889  off2  32572  ofoprabco  32595  indf  32785  tocycf  33081  sgnsf  33126  qqhf  33983  esumcocn  34077  ofcf  34100  mbfmcst  34257  dstrvprob  34470  dstfrvclim1  34476  signstf  34564  fsovfd  44008  dssmapnvod  44016  binomcxplemnotnn0  44352  sge0seq  46451  hoicvrrex  46561