Theorem fmptdf 6751

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1525  Ⅎwnf 1769   ∈ wcel 2083  ∀wral 3107   ↦ cmpt 5047  ⟶wf 6228

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-sep 5101  ax-nul 5108  ax-pr 5228

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3442  df-sbc 3712  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-nul 4218  df-if 4388  df-sn 4479  df-pr 4481  df-op 4485  df-uni 4752  df-br 4969  df-opab 5031  df-mpt 5048  df-id 5355  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-rn 5461  df-res 5462  df-ima 5463  df-iota 6196  df-fun 6234  df-fn 6235  df-f 6236  df-fv 6240

This theorem is referenced by:  gsumesum  30931  voliune  31101  sdclem2  34570  fmptd2f  41067  limsupubuzmpt  41563  xlimmnfmpt  41687  xlimpnfmpt  41688  cncfiooicclem1  41739  dvnprodlem1  41794  stoweidlem35  41884  stoweidlem42  41891  stoweidlem48  41897  stirlinglem8  41930  sge0z  42221  sge0revalmpt  42224  sge0f1o  42228  sge0gerpmpt  42248  sge0ssrempt  42251  sge0ltfirpmpt  42254  sge0lempt  42256  sge0splitmpt  42257  sge0ss  42258  sge0rernmpt  42268  sge0lefimpt  42269  sge0clmpt  42271  sge0ltfirpmpt2  42272  sge0isummpt  42276  sge0xadd  42281  sge0fsummptf  42282  sge0snmptf  42283  sge0ge0mpt  42284  sge0repnfmpt  42285  sge0pnffigtmpt  42286  sge0gtfsumgt  42289  sge0pnfmpt  42291  meadjiun  42312  meaiunlelem  42314  omeiunle  42363  omeiunlempt  42366  opnvonmbllem1  42478  hoimbl2  42511  vonhoire  42518  vonn0ioo2  42536  vonn0icc2  42538  pimgtmnf  42564  issmfdmpt  42589  smfconst  42590  smfadd  42605  smfpimcclem  42645  smflimmpt  42648  smfsupmpt  42653  smfinfmpt  42657  smflimsuplem2  42659  gsumsplit2f  43912  fsuppmptdmf  43931