Theorem fmptdf 7093

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1559  Ⅎwnf 1802   ∈ wcel 2141  ∀wral 3075   ↦ cmpt 5178  ⟶wf 6512

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-pr 5387

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5538  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-fun 6518  df-fn 6519  df-f 6520

This theorem is referenced by:  elrspunidl  33575  gsumesum  34317  voliune  34487  sdclem2  38202  fmptd2f  45771  limsupubuzmpt  46254  xlimmnfmpt  46378  xlimpnfmpt  46379  cncfiooicclem1  46428  stoweidlem35  46570  stoweidlem42  46577  stoweidlem48  46583  stirlinglem8  46616  sge0revalmpt  46913  sge0gerpmpt  46937  sge0ssrempt  46940  sge0ltfirpmpt  46943  sge0lempt  46945  sge0splitmpt  46946  sge0ss  46947  sge0rernmpt  46957  sge0lefimpt  46958  sge0clmpt  46960  sge0ltfirpmpt2  46961  sge0isummpt  46965  sge0xadd  46970  sge0fsummptf  46971  sge0snmptf  46972  sge0ge0mpt  46973  sge0repnfmpt  46974  sge0pnffigtmpt  46975  sge0gtfsumgt  46978  sge0pnfmpt  46980  meadjiun  47001  meaiunlelem  47003  omeiunle  47052  omeiunlempt  47055  opnvonmbllem1  47167  hoimbl2  47200  vonhoire  47207  vonn0ioo2  47225  vonn0icc2  47227  issmfdmpt  47283  smfconst  47284  smfadd  47300  smfpimcclem  47342  smflimmpt  47345  smflimsuplem2  47356  gsumsplit2f  48763  fsuppmptdmf  48961