Theorem fmpt3d 7148

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2147   ↦ cmpt 5192  ⟶wf 6562

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-fun 6568  df-fn 6569  df-f 6570

This theorem is used by:  fmptco  7162  off  7743  caofinvl  7757  curry1f  8154  curry2f  8156  fseqenlem1  10142  indf  12366  pfxf  14872  rpnnen2lem2  16427  1arithlem3  17147  homaf  18255  funcestrcsetclem3  18366  funcsetcestrclem3  18380  prfcl  18427  curf1cl  18452  yonedainv  18505  vrmdf  19104  pmtrf  19720  psgnunilem5  19759  pj1f  19962  vrgpf  20033  gsummptfsadd  20189  gsummptfssub  20214  lspf  21300  uvcff  22152  subrgpsr  22340  mvrf  22347  mhpmulcl  22525  cpm2mf  23125  nmf2  24967  nmof  25093  cphnmf  25571  rrxcph  25768  uniioombllem2  25959  mbfi1fseqlem3  26093  itg2cnlem1  26137  dvmptco  26347  dvle  26382  taylpf  26750  ulmshftlem  26773  ulmshft  26774  ulmdvlem1  26784  psergf  26796  pserdvlem2  26812  logbf  27174  lmif  29347  vtxdgf  30109  brafn  32606  kbop  32612  off2  33333  ofoprabco  33356  tocycf  33777  sgnsf  33822  mplasclco  34259  qqhf  34729  esumcocn  34823  ofcf  34846  mbfmcst  35002  dstrvprob  35215  dstfrvclim1  35221  signstf  35306  fsovfd  45273  dssmapnvod  45281  binomcxplemnotnn0  45601  sge0seq  47729  hoicvr  47831  hoicvrrex  47839  parmapfunc2  51105  parmapfunc  51106