Theorem fmptdf 6875

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1533  Ⅎwnf 1780   ∈ wcel 2110  ∀wral 3138   ↦ cmpt 5138  ⟶wf 6345

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pr 5321

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4561  df-pr 4563  df-op 4567  df-uni 4832  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-fv 6357

This theorem is referenced by:  gsumesum  31313  voliune  31483  sdclem2  35011  fmptd2f  41498  limsupubuzmpt  41993  xlimmnfmpt  42117  xlimpnfmpt  42118  cncfiooicclem1  42169  dvnprodlem1  42224  stoweidlem35  42314  stoweidlem42  42321  stoweidlem48  42327  stirlinglem8  42360  sge0revalmpt  42654  sge0f1o  42658  sge0gerpmpt  42678  sge0ssrempt  42681  sge0ltfirpmpt  42684  sge0lempt  42686  sge0splitmpt  42687  sge0ss  42688  sge0rernmpt  42698  sge0lefimpt  42699  sge0clmpt  42701  sge0ltfirpmpt2  42702  sge0isummpt  42706  sge0xadd  42711  sge0fsummptf  42712  sge0snmptf  42713  sge0ge0mpt  42714  sge0repnfmpt  42715  sge0pnffigtmpt  42716  sge0gtfsumgt  42719  sge0pnfmpt  42721  meadjiun  42742  meaiunlelem  42744  omeiunle  42793  omeiunlempt  42796  opnvonmbllem1  42908  hoimbl2  42941  vonhoire  42948  vonn0ioo2  42966  vonn0icc2  42968  pimgtmnf  42994  issmfdmpt  43019  smfconst  43020  smfadd  43035  smfpimcclem  43075  smflimmpt  43078  smfsupmpt  43083  smfinfmpt  43087  smflimsuplem2  43089  gsumsplit2f  44081  fsuppmptdmf  44423