Theorem fmptdf 7115

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570  Ⅎwnf 1816   ∈ wcel 2145  ∀wral 3077   ↦ cmpt 5186  ⟶wf 6533

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-fun 6539  df-fn 6540  df-f 6541

This theorem is used by:  elrspunidl  33971  gsumesum  34684  voliune  34855  sdclem2  38656  fmptd2f  46216  limsupubuzmpt  46698  xlimmnfmpt  46822  xlimpnfmpt  46823  cncfiooicclem1  46872  stoweidlem35  47014  stoweidlem42  47021  stoweidlem48  47027  stirlinglem8  47060  sge0revalmpt  47357  sge0gerpmpt  47381  sge0ssrempt  47384  sge0ltfirpmpt  47387  sge0lempt  47389  sge0splitmpt  47390  sge0ss  47391  sge0rernmpt  47401  sge0lefimpt  47402  sge0clmpt  47404  sge0ltfirpmpt2  47405  sge0isummpt  47409  sge0xadd  47414  sge0fsummptf  47415  sge0snmptf  47416  sge0ge0mpt  47417  sge0repnfmpt  47418  sge0pnffigtmpt  47419  sge0gtfsumgt  47422  sge0pnfmpt  47424  meadjiun  47445  meaiunlelem  47447  omeiunle  47496  omeiunlempt  47499  opnvonmbllem1  47611  hoimbl2  47644  vonhoire  47651  vonn0ioo2  47669  vonn0icc2  47671  issmfdmpt  47727  smfconst  47728  smfadd  47744  smfpimcclem  47786  smflimmpt  47789  smflimsuplem2  47800  gsumsplit2f  49246  fsuppmptdmf  49459