Theorem fmptdf 7110

Description: A version of fmptd 7107 using bound-variable hypothesis instead of a distinct variable condition for 𝜑. (Contributed by Glauco Siliprandi, 29-Jun-2017.)

Hypotheses

Ref	Expression
fmptdf.1	⊢ Ⅎ𝑥𝜑
fmptdf.2	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)
fmptdf.3	⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)

Assertion

Ref	Expression
fmptdf	⊢ (𝜑 → 𝐹:𝐴⟶𝐶)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐶

Allowed substitution hints:   𝜑(𝑥)   𝐵(𝑥)   𝐹(𝑥)

Proof of Theorem fmptdf

Step	Hyp	Ref	Expression
1		fmptdf.1	. . 3 ⊢ Ⅎ𝑥𝜑
2		fmptdf.2	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)
3	2	ex 417	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐶))
4	1, 3	ralrimi 3269	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶)
5		fmptdf.3	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
6	5	fmpt 7103	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ↔ 𝐹:𝐴⟶𝐶)
7	4, 6	sylib 221	1 ⊢ (𝜑 → 𝐹:𝐴⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567  Ⅎwnf 1810   ∈ wcel 2149  ∀wral 3085   ↦ cmpt 5193  ⟶wf 6529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-pr 5402

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-fun 6535  df-fn 6536  df-f 6537

This theorem is referenced by:  elrspunidl  33676  gsumesum  34390  voliune  34560  sdclem2  38276  fmptd2f  45835  limsupubuzmpt  46318  xlimmnfmpt  46442  xlimpnfmpt  46443  cncfiooicclem1  46492  stoweidlem35  46634  stoweidlem42  46641  stoweidlem48  46647  stirlinglem8  46680  sge0revalmpt  46977  sge0gerpmpt  47001  sge0ssrempt  47004  sge0ltfirpmpt  47007  sge0lempt  47009  sge0splitmpt  47010  sge0ss  47011  sge0rernmpt  47021  sge0lefimpt  47022  sge0clmpt  47024  sge0ltfirpmpt2  47025  sge0isummpt  47029  sge0xadd  47034  sge0fsummptf  47035  sge0snmptf  47036  sge0ge0mpt  47037  sge0repnfmpt  47038  sge0pnffigtmpt  47039  sge0gtfsumgt  47042  sge0pnfmpt  47044  meadjiun  47065  meaiunlelem  47067  omeiunle  47116  omeiunlempt  47119  opnvonmbllem1  47231  hoimbl2  47264  vonhoire  47271  vonn0ioo2  47289  vonn0icc2  47291  issmfdmpt  47347  smfconst  47348  smfadd  47364  smfpimcclem  47406  smflimmpt  47409  smflimsuplem2  47420  gsumsplit2f  48827  fsuppmptdmf  49036