| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > fmpt3d | Structured version Visualization version GIF version | ||
| Description: Domain and codomain of the mapping operation; deduction form. (Contributed by Thierry Arnoux, 4-Jun-2017.) |
| Ref | Expression |
|---|---|
| fmpt3d.1 | ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) |
| fmpt3d.2 | ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) |
| Ref | Expression |
|---|---|
| fmpt3d | ⊢ (𝜑 → 𝐹:𝐴⟶𝐶) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fmpt3d.2 | . . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) | |
| 2 | 1 | fmpttd 7060 | . 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶) |
| 3 | fmpt3d.1 | . . 3 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) | |
| 4 | 3 | feq1d 6644 | . 2 ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶)) |
| 5 | 2, 4 | mpbird 257 | 1 ⊢ (𝜑 → 𝐹:𝐴⟶𝐶) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 = wceq 1541 ∈ wcel 2113 ↦ cmpt 5179 ⟶wf 6488 |
| 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 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-sep 5241 ax-nul 5251 ax-pr 5377 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ral 3052 df-rex 3061 df-rab 3400 df-v 3442 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-nul 4286 df-if 4480 df-sn 4581 df-pr 4583 df-op 4587 df-br 5099 df-opab 5161 df-mpt 5180 df-id 5519 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-fun 6494 df-fn 6495 df-f 6496 |
| This theorem is referenced by: fmptco 7074 off 7640 caofinvl 7654 curry1f 8048 curry2f 8050 fseqenlem1 9934 pfxf 14604 rpnnen2lem2 16140 1arithlem3 16853 homaf 17954 funcestrcsetclem3 18065 funcsetcestrclem3 18079 prfcl 18126 curf1cl 18151 yonedainv 18204 vrmdf 18783 pmtrf 19384 psgnunilem5 19423 pj1f 19626 vrgpf 19697 gsummptfsadd 19853 gsummptfssub 19878 lspf 20925 uvcff 21746 subrgpsr 21933 mvrf 21940 mhpmulcl 22092 cpm2mf 22696 nmf2 24537 nmof 24663 cphnmf 25151 rrxcph 25348 uniioombllem2 25540 mbfi1fseqlem3 25674 itg2cnlem1 25718 dvmptco 25932 dvle 25968 taylpf 26329 ulmshftlem 26354 ulmshft 26355 ulmdvlem1 26365 psergf 26377 pserdvlem2 26394 logbf 26755 lmif 28857 vtxdgf 29545 brafn 32022 kbop 32028 off2 32719 ofoprabco 32742 indf 32934 tocycf 33199 sgnsf 33244 qqhf 34143 esumcocn 34237 ofcf 34260 mbfmcst 34416 dstrvprob 34629 dstfrvclim1 34635 signstf 34723 fsovfd 44253 dssmapnvod 44261 binomcxplemnotnn0 44597 sge0seq 46690 hoicvrrex 46800 |
| Copyright terms: Public domain | W3C validator |