![]() |
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 3975 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → (〈𝑥, 𝑦〉 ∈ 𝐴 → 〈𝑥, 𝑦〉 ∈ 𝐵)) | |
2 | 1 | eximdv 1919 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦〈𝑥, 𝑦〉 ∈ 𝐴 → ∃𝑦〈𝑥, 𝑦〉 ∈ 𝐵)) |
3 | vex 3477 | . . . 4 ⊢ 𝑥 ∈ V | |
4 | 3 | eldm2 5901 | . . 3 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦〈𝑥, 𝑦〉 ∈ 𝐴) |
5 | 3 | eldm2 5901 | . . 3 ⊢ (𝑥 ∈ dom 𝐵 ↔ ∃𝑦〈𝑥, 𝑦〉 ∈ 𝐵) |
6 | 2, 4, 5 | 3imtr4g 296 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ dom 𝐴 → 𝑥 ∈ dom 𝐵)) |
7 | 6 | ssrdv 3988 | 1 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wex 1780 ∈ wcel 2105 ⊆ wss 3948 〈cop 4634 dom cdm 5676 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-sb 2067 df-clab 2709 df-cleq 2723 df-clel 2809 df-rab 3432 df-v 3475 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-br 5149 df-dm 5686 |
This theorem is referenced by: dmeq 5903 dmv 5922 rnss 5938 dmiin 5952 ssxpb 6173 sofld 6186 resssxp 6269 relrelss 6272 funssxp 6746 fndmdif 7043 fneqeql2 7048 dff3 7101 frxp 8117 fnwelem 8122 frxp2 8135 frxp3 8142 funsssuppss 8180 tposss 8218 frrlem8 8284 frrlem14 8290 wfrlem16OLD 8330 smores 8358 smores2 8360 tfrlem13 8396 imafiALT 9351 hartogslem1 9543 wemapso 9552 dmttrcl 9722 r0weon 10013 infxpenlem 10014 brdom3 10529 brdom5 10530 brdom4 10531 fpwwe2lem12 10643 fpwwe2 10644 canth4 10648 canthwelem 10651 pwfseqlem4 10663 nqerf 10931 dmrecnq 10969 uzrdgfni 13930 hashdmpropge2 14451 dmtrclfv 14972 rlimpm 15451 isstruct2 17089 strleun 17097 imasaddfnlem 17481 imasvscafn 17490 isohom 17730 catcoppccl 18077 catcoppcclOLD 18078 tsrss 18552 ledm 18553 dirdm 18563 f1omvdmvd 19359 mvdco 19361 f1omvdconj 19362 pmtrfb 19381 pmtrfconj 19382 symggen 19386 symggen2 19387 pmtrdifellem1 19392 pmtrdifellem2 19393 psgnunilem1 19409 gsum2d 19888 lspextmo 20900 dsmmfi 21604 lindfres 21689 mdetdiaglem 22421 tsmsxp 23980 ustssco 24040 setsmstopn 24307 metustexhalf 24386 tngtopn 24488 equivcau 25149 metsscmetcld 25164 dvbssntr 25750 pserdv 26282 subgreldmiedg 28975 hlimcaui 30924 nfpconfp 32291 symgcom2 32683 pmtrcnel 32688 pmtrcnel2 32689 pmtrcnelor 32690 cycpmrn 32740 metideq 33339 esum2d 33557 subgrwlk 34589 fundmpss 35210 fixssdm 35350 filnetlem3 35732 filnetlem4 35733 ssbnd 37123 bnd2lem 37126 ismrcd1 41902 istopclsd 41904 mptrcllem 42830 cnvrcl0 42842 dmtrcl 42844 dfrcl2 42891 relexpss1d 42922 rfovcnvf1od 43221 fourierdlem80 45364 issmflem 45905 |
Copyright terms: Public domain | W3C validator |