![]() |
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 6748 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 413 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐶)) |
4 | 1, 3 | ralrimi 3185 | . 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶) |
5 | fmptdf.3 | . . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) | |
6 | 5 | fmpt 6744 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ↔ 𝐹:𝐴⟶𝐶) |
7 | 4, 6 | sylib 219 | 1 ⊢ (𝜑 → 𝐹:𝐴⟶𝐶) |
Colors of variables: wff setvar class |
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 |
Copyright terms: Public domain | W3C validator |