![]() |
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 6700 | . 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶) |
3 | fmpt3d.1 | . . 3 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) | |
4 | 3 | feq1d 6326 | . 2 ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶)) |
5 | 2, 4 | mpbird 249 | 1 ⊢ (𝜑 → 𝐹:𝐴⟶𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 = wceq 1507 ∈ wcel 2050 ↦ cmpt 5004 ⟶wf 6181 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2744 ax-sep 5056 ax-nul 5063 ax-pr 5182 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2584 df-clab 2753 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ne 2962 df-ral 3087 df-rex 3088 df-rab 3091 df-v 3411 df-sbc 3676 df-dif 3826 df-un 3828 df-in 3830 df-ss 3837 df-nul 4173 df-if 4345 df-sn 4436 df-pr 4438 df-op 4442 df-uni 4709 df-br 4926 df-opab 4988 df-mpt 5005 df-id 5308 df-xp 5409 df-rel 5410 df-cnv 5411 df-co 5412 df-dm 5413 df-rn 5414 df-res 5415 df-ima 5416 df-iota 6149 df-fun 6187 df-fn 6188 df-f 6189 df-fv 6193 |
This theorem is referenced by: fmptco 6712 off 7240 caofinvl 7252 curry1f 7607 curry2f 7609 fseqenlem1 9242 pfxf 13860 rpnnen2lem2 15426 1arithlem3 16115 homaf 17160 funcestrcsetclem3 17262 funcsetcestrclem3 17276 prfcl 17323 curf1cl 17348 yonedainv 17401 vrmdf 17876 pmtrf 18356 psgnunilem5 18395 pj1f 18593 vrgpf 18666 gsummptfsadd 18809 gsummptfssub 18834 lspf 19480 subrgpsr 19925 mvrf 19930 uvcff 20649 cpm2mf 21076 nmf2 22917 nmof 23043 cphnmf 23514 rrxcph 23710 uniioombllem2 23899 mbfi1fseqlem3 24033 itg2cnlem1 24077 dvmptco 24284 dvle 24319 taylpf 24669 ulmshftlem 24692 ulmshft 24693 ulmdvlem1 24703 psergf 24715 pserdvlem2 24731 logbf 25080 lmif 26285 vtxdgf 26968 brafn 29517 kbop 29523 off2 30164 ofoprabco 30185 tocycf 30476 sgnsf 30499 qqhf 30900 indf 30947 esumcocn 31012 ofcf 31035 mbfmcst 31191 dstrvprob 31404 dstfrvclim1 31410 signstf 31511 fsovfd 39750 dssmapnvod 39758 binomcxplemnotnn0 40133 sge0seq 42184 hoicvrrex 42294 |
Copyright terms: Public domain | W3C validator |