![]() |
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 5969 | . 2 ⊢ dom 𝐹 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} |
3 | 2 | ssrab3 3978 | 1 ⊢ dom 𝐹 ⊆ 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1522 ∈ wcel 2081 Vcvv 3437 ⊆ wss 3859 ↦ cmpt 5041 dom cdm 5443 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-sep 5094 ax-nul 5101 ax-pr 5221 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ral 3110 df-rab 3114 df-v 3439 df-dif 3862 df-un 3864 df-in 3866 df-ss 3874 df-nul 4212 df-if 4382 df-sn 4473 df-pr 4475 df-op 4479 df-br 4963 df-opab 5025 df-mpt 5042 df-xp 5449 df-rel 5450 df-cnv 5451 df-dm 5453 df-rn 5454 df-res 5455 df-ima 5456 |
This theorem is referenced by: mptrcl 6643 fvmptss 6646 fvmptex 6648 fvmptnf 6656 elfvmptrab1 6660 mptexg 6850 mptexw 7510 dmmpossx 7620 tposssxp 7747 mptfi 8669 cnvimamptfin 8671 cantnfres 8986 mptct 9806 arwrcl 17133 cntzrcl 18198 gsumconst 18774 psrass1lem 19845 psrass1 19873 psrass23l 19876 psrcom 19877 psrass23 19878 mpfrcl 19985 psropprmul 20089 coe1mul2 20120 lmrcl 21523 1stcrestlem 21744 ptbasfi 21873 isxms2 22741 setsmstopn 22771 tngtopn 22942 rrxmval 23691 ulmss 24668 dchrrcl 25498 gsummpt2co 30495 locfinreflem 30721 sitgclg 31217 cvmsrcl 32119 snmlval 32186 gonan0 32247 bj-fvmptunsn1 34097 eldiophb 38839 elmnc 39221 itgocn 39249 submgmrcl 43531 dmmpossx2 43863 |
Copyright terms: Public domain | W3C validator |