![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fconst6 | Structured version Visualization version GIF version |
Description: A constant function as a mapping. (Contributed by Jeff Madsen, 30-Nov-2009.) (Revised by Mario Carneiro, 22-Apr-2015.) |
Ref | Expression |
---|---|
fconst6.1 | ⊢ 𝐵 ∈ 𝐶 |
Ref | Expression |
---|---|
fconst6 | ⊢ (𝐴 × {𝐵}):𝐴⟶𝐶 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fconst6.1 | . 2 ⊢ 𝐵 ∈ 𝐶 | |
2 | fconst6g 6308 | . 2 ⊢ (𝐵 ∈ 𝐶 → (𝐴 × {𝐵}):𝐴⟶𝐶) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 × {𝐵}):𝐴⟶𝐶 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2157 {csn 4367 × cxp 5309 ⟶wf 6096 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2377 ax-ext 2776 ax-sep 4974 ax-nul 4982 ax-pr 5096 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2591 df-eu 2609 df-clab 2785 df-cleq 2791 df-clel 2794 df-nfc 2929 df-ne 2971 df-ral 3093 df-rab 3097 df-v 3386 df-dif 3771 df-un 3773 df-in 3775 df-ss 3782 df-nul 4115 df-if 4277 df-sn 4368 df-pr 4370 df-op 4374 df-br 4843 df-opab 4905 df-mpt 4922 df-id 5219 df-xp 5317 df-rel 5318 df-cnv 5319 df-co 5320 df-dm 5321 df-rn 5322 df-fun 6102 df-fn 6103 df-f 6104 |
This theorem is referenced by: ramz 16059 psrlidm 19723 psrbag0 19813 00ply1bas 19929 ply1plusgfvi 19931 mbfpos 23756 i1f0 23792 axlowdimlem1 26172 axlowdimlem7 26178 axlowdim1 26189 hlim0 28610 0cnfn 29357 0lnfn 29362 circlemethnat 31232 circlevma 31233 noxp1o 32322 poimirlem29 33920 poimirlem30 33921 poimirlem31 33922 poimir 33924 broucube 33925 expgrowth 39305 |
Copyright terms: Public domain | W3C validator |