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 6878 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 415 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐶)) |
4 | 1, 3 | ralrimi 3216 | . 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶) |
5 | fmptdf.3 | . . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) | |
6 | 5 | fmpt 6874 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ↔ 𝐹:𝐴⟶𝐶) |
7 | 4, 6 | sylib 220 | 1 ⊢ (𝜑 → 𝐹:𝐴⟶𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 = wceq 1537 Ⅎwnf 1784 ∈ wcel 2114 ∀wral 3138 ↦ cmpt 5146 ⟶wf 6351 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-sep 5203 ax-nul 5210 ax-pr 5330 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 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 3773 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-nul 4292 df-if 4468 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4839 df-br 5067 df-opab 5129 df-mpt 5147 df-id 5460 df-xp 5561 df-rel 5562 df-cnv 5563 df-co 5564 df-dm 5565 df-rn 5566 df-res 5567 df-ima 5568 df-iota 6314 df-fun 6357 df-fn 6358 df-f 6359 df-fv 6363 |
This theorem is referenced by: gsumesum 31318 voliune 31488 sdclem2 35032 fmptd2f 41525 limsupubuzmpt 42020 xlimmnfmpt 42144 xlimpnfmpt 42145 cncfiooicclem1 42196 dvnprodlem1 42251 stoweidlem35 42340 stoweidlem42 42347 stoweidlem48 42353 stirlinglem8 42386 sge0revalmpt 42680 sge0f1o 42684 sge0gerpmpt 42704 sge0ssrempt 42707 sge0ltfirpmpt 42710 sge0lempt 42712 sge0splitmpt 42713 sge0ss 42714 sge0rernmpt 42724 sge0lefimpt 42725 sge0clmpt 42727 sge0ltfirpmpt2 42728 sge0isummpt 42732 sge0xadd 42737 sge0fsummptf 42738 sge0snmptf 42739 sge0ge0mpt 42740 sge0repnfmpt 42741 sge0pnffigtmpt 42742 sge0gtfsumgt 42745 sge0pnfmpt 42747 meadjiun 42768 meaiunlelem 42770 omeiunle 42819 omeiunlempt 42822 opnvonmbllem1 42934 hoimbl2 42967 vonhoire 42974 vonn0ioo2 42992 vonn0icc2 42994 pimgtmnf 43020 issmfdmpt 43045 smfconst 43046 smfadd 43061 smfpimcclem 43101 smflimmpt 43104 smfsupmpt 43109 smfinfmpt 43113 smflimsuplem2 43115 gsumsplit2f 44107 fsuppmptdmf 44449 |
Copyright terms: Public domain | W3C validator |