![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fmptdf | Structured version Visualization version GIF version |
Description: A version of fmptd 7133 using bound-variable hypothesis instead of a distinct variable condition for 𝜑. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
Ref | Expression |
---|---|
fmptdf.1 | ⊢ Ⅎ𝑥𝜑 |
fmptdf.2 | ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) |
fmptdf.3 | ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) |
Ref | Expression |
---|---|
fmptdf | ⊢ (𝜑 → 𝐹:𝐴⟶𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fmptdf.1 | . . 3 ⊢ Ⅎ𝑥𝜑 | |
2 | fmptdf.2 | . . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) | |
3 | 2 | ex 412 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐶)) |
4 | 1, 3 | ralrimi 3254 | . 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶) |
5 | fmptdf.3 | . . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) | |
6 | 5 | fmpt 7129 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ↔ 𝐹:𝐴⟶𝐶) |
7 | 4, 6 | sylib 218 | 1 ⊢ (𝜑 → 𝐹:𝐴⟶𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 = wceq 1536 Ⅎwnf 1779 ∈ wcel 2105 ∀wral 3058 ↦ cmpt 5230 ⟶wf 6558 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-10 2138 ax-11 2154 ax-12 2174 ax-ext 2705 ax-sep 5301 ax-nul 5311 ax-pr 5437 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-nf 1780 df-sb 2062 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2726 df-clel 2813 df-nfc 2889 df-ral 3059 df-rex 3068 df-rab 3433 df-v 3479 df-dif 3965 df-un 3967 df-in 3969 df-ss 3979 df-nul 4339 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-br 5148 df-opab 5210 df-mpt 5231 df-id 5582 df-xp 5694 df-rel 5695 df-cnv 5696 df-co 5697 df-dm 5698 df-rn 5699 df-res 5700 df-ima 5701 df-fun 6564 df-fn 6565 df-f 6566 |
This theorem is referenced by: elrspunidl 33435 gsumesum 34039 voliune 34209 sdclem2 37728 fmptd2f 45177 limsupubuzmpt 45674 xlimmnfmpt 45798 xlimpnfmpt 45799 cncfiooicclem1 45848 stoweidlem35 45990 stoweidlem42 45997 stoweidlem48 46003 stirlinglem8 46036 sge0revalmpt 46333 sge0gerpmpt 46357 sge0ssrempt 46360 sge0ltfirpmpt 46363 sge0lempt 46365 sge0splitmpt 46366 sge0ss 46367 sge0rernmpt 46377 sge0lefimpt 46378 sge0clmpt 46380 sge0ltfirpmpt2 46381 sge0isummpt 46385 sge0xadd 46390 sge0fsummptf 46391 sge0snmptf 46392 sge0ge0mpt 46393 sge0repnfmpt 46394 sge0pnffigtmpt 46395 sge0gtfsumgt 46398 sge0pnfmpt 46400 meadjiun 46421 meaiunlelem 46423 omeiunle 46472 omeiunlempt 46475 opnvonmbllem1 46587 hoimbl2 46620 vonhoire 46627 vonn0ioo2 46645 vonn0icc2 46647 issmfdmpt 46703 smfconst 46704 smfadd 46720 smfpimcclem 46762 smflimmpt 46765 smflimsuplem2 46776 gsumsplit2f 48023 fsuppmptdmf 48222 |
Copyright terms: Public domain | W3C validator |