Theorem dmss 5911

Description: Subset theorem for domain. (Contributed by NM, 11-Aug-1994.)

Assertion

Ref	Expression
dmss	⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)

Proof of Theorem dmss

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssel 3976	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
2	1	eximdv 1917	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴 → ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵))
3		vex 3483	. . . 4 ⊢ 𝑥 ∈ V
4	3	eldm2 5910	. . 3 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
5	3	eldm2 5910	. . 3 ⊢ (𝑥 ∈ dom 𝐵 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵)
6	2, 4, 5	3imtr4g 296	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ dom 𝐴 → 𝑥 ∈ dom 𝐵))
7	6	ssrdv 3988	1 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)

Syntax hints:   → wi 4  ∃wex 1779   ∈ wcel 2108   ⊆ wss 3950  ⟨cop 4630  dom cdm 5683

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-br 5142  df-dm 5693

This theorem is referenced by:  dmeq  5912  dmv  5931  rnss  5948  dmiin  5962  dmresss  6027  ssxpb  6192  sofld  6205  resssxp  6288  relrelss  6291  funssxp  6762  fndmdif  7060  fneqeql2  7065  dff3  7118  frxp  8147  fnwelem  8152  frxp2  8165  frxp3  8172  funsssuppss  8211  tposss  8248  frrlem8  8314  frrlem14  8320  wfrlem16OLD  8360  smores  8388  smores2  8390  tfrlem13  8426  imafi  9349  hartogslem1  9578  wemapso  9587  dmttrcl  9757  r0weon  10048  infxpenlem  10049  brdom3  10564  brdom5  10565  brdom4  10566  fpwwe2lem12  10678  fpwwe2  10679  canth4  10683  canthwelem  10686  pwfseqlem4  10698  nqerf  10966  dmrecnq  11004  uzrdgfni  13995  hashdmpropge2  14518  dmtrclfv  15053  rlimpm  15532  isstruct2  17182  strleun  17190  imasaddfnlem  17569  imasvscafn  17578  isohom  17816  catcoppccl  18158  tsrss  18630  ledm  18631  dirdm  18641  f1omvdmvd  19457  mvdco  19459  f1omvdconj  19460  pmtrfb  19479  pmtrfconj  19480  symggen  19484  symggen2  19485  pmtrdifellem1  19490  pmtrdifellem2  19491  psgnunilem1  19507  gsum2d  19986  lspextmo  21047  dsmmfi  21750  lindfres  21835  mdetdiaglem  22594  tsmsxp  24153  ustssco  24213  setsmstopn  24480  metustexhalf  24559  tngtopn  24661  equivcau  25324  metsscmetcld  25339  dvbssntr  25925  pserdv  26463  noseqrdgfn  28302  subgreldmiedg  29290  hlimcaui  31245  nfpconfp  32631  gsumfs2d  33043  symgcom2  33089  pmtrcnel  33094  pmtrcnel2  33095  pmtrcnelor  33096  cycpmrn  33148  metideq  33870  esum2d  34072  subgrwlk  35115  fundmpss  35745  fixssdm  35885  filnetlem3  36359  filnetlem4  36360  ssbnd  37773  bnd2lem  37776  ismrcd1  42687  istopclsd  42689  mptrcllem  43604  cnvrcl0  43616  dmtrcl  43618  dfrcl2  43665  relexpss1d  43696  rfovcnvf1od  43995  fourierdlem80  46174  issmflem  46715