| 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 7135 | . 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶) |
| 3 | fmpt3d.1 | . . 3 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) | |
| 4 | 3 | feq1d 6720 | . 2 ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶)) |
| 5 | 2, 4 | mpbird 257 | 1 ⊢ (𝜑 → 𝐹:𝐴⟶𝐶) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2108 ↦ cmpt 5225 ⟶wf 6557 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pr 5432 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-br 5144 df-opab 5206 df-mpt 5226 df-id 5578 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-fun 6563 df-fn 6564 df-f 6565 |
| This theorem is referenced by: fmptco 7149 off 7715 caofinvl 7729 curry1f 8131 curry2f 8133 fseqenlem1 10064 pfxf 14718 rpnnen2lem2 16251 1arithlem3 16963 homaf 18075 funcestrcsetclem3 18187 funcsetcestrclem3 18201 prfcl 18248 curf1cl 18273 yonedainv 18326 vrmdf 18871 pmtrf 19473 psgnunilem5 19512 pj1f 19715 vrgpf 19786 gsummptfsadd 19942 gsummptfssub 19967 lspf 20972 uvcff 21811 subrgpsr 21998 mvrf 22005 mhpmulcl 22153 cpm2mf 22758 nmf2 24606 nmof 24740 cphnmf 25229 rrxcph 25426 uniioombllem2 25618 mbfi1fseqlem3 25752 itg2cnlem1 25796 dvmptco 26010 dvle 26046 taylpf 26407 ulmshftlem 26432 ulmshft 26433 ulmdvlem1 26443 psergf 26455 pserdvlem2 26472 logbf 26832 lmif 28793 vtxdgf 29489 brafn 31966 kbop 31972 off2 32651 ofoprabco 32674 indf 32840 tocycf 33137 sgnsf 33182 qqhf 33987 esumcocn 34081 ofcf 34104 mbfmcst 34261 dstrvprob 34474 dstfrvclim1 34480 signstf 34581 fsovfd 44025 dssmapnvod 44033 binomcxplemnotnn0 44375 sge0seq 46461 hoicvrrex 46571 |
| Copyright terms: Public domain | W3C validator |