Theorem fmptdf 7114

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570  Ⅎwnf 1813   ∈ wcel 2143  ∀wral 3079   ↦ cmpt 5193  ⟶wf 6534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-fun 6540  df-fn 6541  df-f 6542

This theorem is referenced by:  elrspunidl  33717  gsumesum  34430  voliune  34600  sdclem2  38374  fmptd2f  45933  limsupubuzmpt  46416  xlimmnfmpt  46540  xlimpnfmpt  46541  cncfiooicclem1  46590  stoweidlem35  46732  stoweidlem42  46739  stoweidlem48  46745  stirlinglem8  46778  sge0revalmpt  47075  sge0gerpmpt  47099  sge0ssrempt  47102  sge0ltfirpmpt  47105  sge0lempt  47107  sge0splitmpt  47108  sge0ss  47109  sge0rernmpt  47119  sge0lefimpt  47120  sge0clmpt  47122  sge0ltfirpmpt2  47123  sge0isummpt  47127  sge0xadd  47132  sge0fsummptf  47133  sge0snmptf  47134  sge0ge0mpt  47135  sge0repnfmpt  47136  sge0pnffigtmpt  47137  sge0gtfsumgt  47140  sge0pnfmpt  47142  meadjiun  47163  meaiunlelem  47165  omeiunle  47214  omeiunlempt  47217  opnvonmbllem1  47329  hoimbl2  47362  vonhoire  47369  vonn0ioo2  47387  vonn0icc2  47389  issmfdmpt  47445  smfconst  47446  smfadd  47462  smfpimcclem  47504  smflimmpt  47507  smflimsuplem2  47518  gsumsplit2f  48928  fsuppmptdmf  49141