![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dmss | Structured version Visualization version GIF version |
Description: Subset theorem for domain. (Contributed by NM, 11-Aug-1994.) |
Ref | Expression |
---|---|
dmss | ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssel 3738 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → (〈𝑥, 𝑦〉 ∈ 𝐴 → 〈𝑥, 𝑦〉 ∈ 𝐵)) | |
2 | 1 | eximdv 1995 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦〈𝑥, 𝑦〉 ∈ 𝐴 → ∃𝑦〈𝑥, 𝑦〉 ∈ 𝐵)) |
3 | vex 3343 | . . . 4 ⊢ 𝑥 ∈ V | |
4 | 3 | eldm2 5477 | . . 3 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦〈𝑥, 𝑦〉 ∈ 𝐴) |
5 | 3 | eldm2 5477 | . . 3 ⊢ (𝑥 ∈ dom 𝐵 ↔ ∃𝑦〈𝑥, 𝑦〉 ∈ 𝐵) |
6 | 2, 4, 5 | 3imtr4g 285 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ dom 𝐴 → 𝑥 ∈ dom 𝐵)) |
7 | 6 | ssrdv 3750 | 1 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wex 1853 ∈ wcel 2139 ⊆ wss 3715 〈cop 4327 dom cdm 5266 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-9 2148 ax-10 2168 ax-11 2183 ax-12 2196 ax-13 2391 ax-ext 2740 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2047 df-clab 2747 df-cleq 2753 df-clel 2756 df-nfc 2891 df-rab 3059 df-v 3342 df-dif 3718 df-un 3720 df-in 3722 df-ss 3729 df-nul 4059 df-if 4231 df-sn 4322 df-pr 4324 df-op 4328 df-br 4805 df-dm 5276 |
This theorem is referenced by: dmeq 5479 dmv 5496 rnss 5509 dmiin 5524 ssxpb 5726 sofld 5739 relrelss 5820 funssxp 6222 fndmdif 6484 fneqeql2 6489 dff3 6535 frxp 7455 fnwelem 7460 funsssuppss 7490 tposss 7522 wfrlem16 7599 smores 7618 smores2 7620 tfrlem13 7655 imafi 8424 hartogslem1 8612 wemapso 8621 r0weon 9025 infxpenlem 9026 brdom3 9542 brdom5 9543 brdom4 9544 fpwwe2lem13 9656 fpwwe2 9657 canth4 9661 canthwelem 9664 pwfseqlem4 9676 nqerf 9944 dmrecnq 9982 uzrdgfni 12951 hashdmpropge2 13457 dmtrclfv 13958 rlimpm 14430 isstruct2 16069 strlemor1OLD 16171 strleun 16174 imasaddfnlem 16390 imasvscafn 16399 isohom 16637 catcoppccl 16959 tsrss 17424 ledm 17425 dirdm 17435 f1omvdmvd 18063 mvdco 18065 f1omvdconj 18066 pmtrfb 18085 pmtrfconj 18086 symggen 18090 symggen2 18091 pmtrdifellem1 18096 pmtrdifellem2 18097 psgnunilem1 18113 gsum2d 18571 lspextmo 19258 dsmmfi 20284 lindfres 20364 mdetdiaglem 20606 tsmsxp 22159 ustssco 22219 setsmstopn 22484 metustexhalf 22562 tngtopn 22655 equivcau 23298 cmetss 23313 dvbssntr 23863 pserdv 24382 structgrssvtxlemOLD 26114 subgreldmiedg 26374 hlimcaui 28402 metideq 30245 esum2d 30464 fundmpss 31971 fixssdm 32319 filnetlem3 32681 filnetlem4 32682 ssbnd 33900 bnd2lem 33903 ismrcd1 37763 istopclsd 37765 mptrcllem 38422 cnvrcl0 38434 dmtrcl 38436 dfrcl2 38468 relexpss1d 38499 rp-imass 38567 rfovcnvf1od 38800 fourierdlem80 40906 issmflem 41442 |
Copyright terms: Public domain | W3C validator |