Theorem fmptdf 7118

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569  Ⅎwnf 1815   ∈ wcel 2144  ∀wral 3076   ↦ cmpt 5185  ⟶wf 6535

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-fun 6541  df-fn 6542  df-f 6543

This theorem is used by:  elrspunidl  34025  gsumesum  34738  voliune  34909  sdclem2  38770  fmptd2f  46341  limsupubuzmpt  46823  xlimmnfmpt  46947  xlimpnfmpt  46948  cncfiooicclem1  46997  stoweidlem35  47139  stoweidlem42  47146  stoweidlem48  47152  stirlinglem8  47185  sge0revalmpt  47482  sge0gerpmpt  47506  sge0ssrempt  47509  sge0ltfirpmpt  47512  sge0lempt  47514  sge0splitmpt  47515  sge0ss  47516  sge0rernmpt  47526  sge0lefimpt  47527  sge0clmpt  47529  sge0ltfirpmpt2  47530  sge0isummpt  47534  sge0xadd  47539  sge0fsummptf  47540  sge0snmptf  47541  sge0ge0mpt  47542  sge0repnfmpt  47543  sge0pnffigtmpt  47544  sge0gtfsumgt  47547  sge0pnfmpt  47549  meadjiun  47570  meaiunlelem  47572  omeiunle  47621  omeiunlempt  47624  opnvonmbllem1  47736  hoimbl2  47769  vonhoire  47776  vonn0ioo2  47794  vonn0icc2  47796  issmfdmpt  47852  smfconst  47853  smfadd  47869  smfpimcclem  47911  smflimmpt  47914  smflimsuplem2  47925  gsumsplit2f  49371  fsuppmptdmf  49584