![]() |
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 7124 | . 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶) |
3 | fmpt3d.1 | . . 3 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) | |
4 | 3 | feq1d 6708 | . 2 ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶)) |
5 | 2, 4 | mpbird 256 | 1 ⊢ (𝜑 → 𝐹:𝐴⟶𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 = wceq 1533 ∈ wcel 2098 ↦ cmpt 5232 ⟶wf 6545 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-sep 5300 ax-nul 5307 ax-pr 5429 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ral 3051 df-rex 3060 df-rab 3419 df-v 3463 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4323 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-br 5150 df-opab 5212 df-mpt 5233 df-id 5576 df-xp 5684 df-rel 5685 df-cnv 5686 df-co 5687 df-dm 5688 df-rn 5689 df-res 5690 df-ima 5691 df-fun 6551 df-fn 6552 df-f 6553 |
This theorem is referenced by: fmptco 7138 off 7703 caofinvl 7716 curry1f 8111 curry2f 8113 fseqenlem1 10054 pfxf 14671 rpnnen2lem2 16200 1arithlem3 16902 homaf 18027 funcestrcsetclem3 18141 funcsetcestrclem3 18155 prfcl 18202 curf1cl 18228 yonedainv 18281 vrmdf 18823 pmtrf 19427 psgnunilem5 19466 pj1f 19669 vrgpf 19740 gsummptfsadd 19896 gsummptfssub 19921 lspf 20875 uvcff 21747 subrgpsr 21945 mvrf 21952 mhpmulcl 22101 cpm2mf 22703 nmf2 24551 nmof 24685 cphnmf 25172 rrxcph 25369 uniioombllem2 25561 mbfi1fseqlem3 25696 itg2cnlem1 25740 dvmptco 25953 dvle 25989 taylpf 26350 ulmshftlem 26375 ulmshft 26376 ulmdvlem1 26386 psergf 26398 pserdvlem2 26415 logbf 26771 lmif 28666 vtxdgf 29362 brafn 31834 kbop 31840 off2 32513 ofoprabco 32536 tocycf 32935 sgnsf 32980 qqhf 33720 indf 33767 esumcocn 33832 ofcf 33855 mbfmcst 34012 dstrvprob 34224 dstfrvclim1 34230 signstf 34331 fsovfd 43586 dssmapnvod 43594 binomcxplemnotnn0 43937 sge0seq 45974 hoicvrrex 46084 |
Copyright terms: Public domain | W3C validator |