Theorem fmptdf 7045

Description: A version of fmptd 7042 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 412	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐶))
4	1, 3	ralrimi 3230	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶)
5		fmptdf.3	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
6	5	fmpt 7038	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ↔ 𝐹:𝐴⟶𝐶)
7	4, 6	sylib 218	1 ⊢ (𝜑 → 𝐹:𝐴⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541  Ⅎwnf 1784   ∈ wcel 2111  ∀wral 3047   ↦ cmpt 5167  ⟶wf 6472

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pr 5365

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5506  df-xp 5617  df-rel 5618  df-cnv 5619  df-co 5620  df-dm 5621  df-rn 5622  df-res 5623  df-ima 5624  df-fun 6478  df-fn 6479  df-f 6480

This theorem is referenced by:  elrspunidl  33385  gsumesum  34064  voliune  34234  sdclem2  37782  fmptd2f  45272  limsupubuzmpt  45757  xlimmnfmpt  45881  xlimpnfmpt  45882  cncfiooicclem1  45931  stoweidlem35  46073  stoweidlem42  46080  stoweidlem48  46086  stirlinglem8  46119  sge0revalmpt  46416  sge0gerpmpt  46440  sge0ssrempt  46443  sge0ltfirpmpt  46446  sge0lempt  46448  sge0splitmpt  46449  sge0ss  46450  sge0rernmpt  46460  sge0lefimpt  46461  sge0clmpt  46463  sge0ltfirpmpt2  46464  sge0isummpt  46468  sge0xadd  46473  sge0fsummptf  46474  sge0snmptf  46475  sge0ge0mpt  46476  sge0repnfmpt  46477  sge0pnffigtmpt  46478  sge0gtfsumgt  46481  sge0pnfmpt  46483  meadjiun  46504  meaiunlelem  46506  omeiunle  46555  omeiunlempt  46558  opnvonmbllem1  46670  hoimbl2  46703  vonhoire  46710  vonn0ioo2  46728  vonn0icc2  46730  issmfdmpt  46786  smfconst  46787  smfadd  46803  smfpimcclem  46845  smflimmpt  46848  smflimsuplem2  46859  gsumsplit2f  48211  fsuppmptdmf  48409