![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dmmptss | Structured version Visualization version GIF version |
Description: The domain of a mapping is a subset of its base class. (Contributed by Scott Fenton, 17-Jun-2013.) |
Ref | Expression |
---|---|
dmmpt.1 | ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) |
Ref | Expression |
---|---|
dmmptss | ⊢ dom 𝐹 ⊆ 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dmmpt.1 | . . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) | |
2 | 1 | dmmpt 5789 | . 2 ⊢ dom 𝐹 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} |
3 | ssrab2 3826 | . 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} ⊆ 𝐴 | |
4 | 2, 3 | eqsstri 3774 | 1 ⊢ dom 𝐹 ⊆ 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1630 ∈ wcel 2137 {crab 3052 Vcvv 3338 ⊆ wss 3713 ↦ cmpt 4879 dom cdm 5264 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1869 ax-4 1884 ax-5 1986 ax-6 2052 ax-7 2088 ax-9 2146 ax-10 2166 ax-11 2181 ax-12 2194 ax-13 2389 ax-ext 2738 ax-sep 4931 ax-nul 4939 ax-pr 5053 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1633 df-ex 1852 df-nf 1857 df-sb 2045 df-eu 2609 df-mo 2610 df-clab 2745 df-cleq 2751 df-clel 2754 df-nfc 2889 df-ral 3053 df-rab 3057 df-v 3340 df-dif 3716 df-un 3718 df-in 3720 df-ss 3727 df-nul 4057 df-if 4229 df-sn 4320 df-pr 4322 df-op 4326 df-br 4803 df-opab 4863 df-mpt 4880 df-xp 5270 df-rel 5271 df-cnv 5272 df-dm 5274 df-rn 5275 df-res 5276 df-ima 5277 |
This theorem is referenced by: mptrcl 6449 fvmptss 6452 fvmptex 6454 fvmptnf 6462 elfvmptrab1 6465 mptexg 6646 dmmpt2ssx 7401 curry1val 7436 curry2val 7440 tposssxp 7523 mptfi 8428 cnvimamptfin 8430 cantnfres 8745 mptct 9550 bitsval 15346 subcrcl 16675 arwval 16892 arwrcl 16893 coafval 16913 submrcl 17545 issubg 17793 isnsg 17822 cntzrcl 17958 gsumconst 18532 abvrcl 19021 psrass1lem 19577 psrass1 19605 psrass23l 19608 psrcom 19609 psrass23 19610 mpfrcl 19718 psropprmul 19808 coe1mul2 19839 isobs 20264 lmrcl 21235 1stcrestlem 21455 islocfin 21520 kgeni 21540 ptbasfi 21584 isxms2 22452 setsmstopn 22482 tngtopn 22653 isphtpc 22992 pcofval 23008 cfili 23264 cfilfcls 23270 rrxmval 23386 plybss 24147 ulmss 24348 dchrrcl 25162 gsummpt2co 30087 locfinreflem 30214 sitgclg 30711 cvmsrcl 31551 snmlval 31618 eldiophb 37820 elmnc 38206 itgocn 38234 issdrg 38267 submgmrcl 42290 dmmpt2ssx2 42623 |
Copyright terms: Public domain | W3C validator |