Theorem dmss 5851

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 3927	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
2	1	eximdv 1918	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴 → ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵))
3		vex 3444	. . . 4 ⊢ 𝑥 ∈ V
4	3	eldm2 5850	. . 3 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
5	3	eldm2 5850	. . 3 ⊢ (𝑥 ∈ dom 𝐵 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵)
6	2, 4, 5	3imtr4g 296	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ dom 𝐴 → 𝑥 ∈ dom 𝐵))
7	6	ssrdv 3939	1 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)

Syntax hints:   → wi 4  ∃wex 1780   ∈ wcel 2113   ⊆ wss 3901  ⟨cop 4586  dom cdm 5624

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-dm 5634

This theorem is referenced by:  dmeq  5852  dmv  5871  rnss  5888  dmiin  5902  dmresss  5970  ssxpb  6132  sofld  6145  resssxp  6228  relrelss  6231  funssxp  6690  fndmdif  6987  fneqeql2  6992  dff3  7045  frxp  8068  fnwelem  8073  frxp2  8086  frxp3  8093  funsssuppss  8132  tposss  8169  frrlem8  8235  frrlem14  8241  smores  8284  smores2  8286  tfrlem13  8321  imafi  9215  hartogslem1  9447  wemapso  9456  dmttrcl  9630  r0weon  9922  infxpenlem  9923  brdom3  10438  brdom5  10439  brdom4  10440  fpwwe2lem12  10553  fpwwe2  10554  canth4  10558  canthwelem  10561  pwfseqlem4  10573  nqerf  10841  dmrecnq  10879  uzrdgfni  13881  hashdmpropge2  14406  dmtrclfv  14941  rlimpm  15423  isstruct2  17076  strleun  17084  imasaddfnlem  17449  imasvscafn  17458  isohom  17700  catcoppccl  18041  tsrss  18512  ledm  18513  dirdm  18523  f1omvdmvd  19372  mvdco  19374  f1omvdconj  19375  pmtrfb  19394  pmtrfconj  19395  symggen  19399  symggen2  19400  pmtrdifellem1  19405  pmtrdifellem2  19406  psgnunilem1  19422  gsum2d  19901  lspextmo  21008  dsmmfi  21693  lindfres  21778  mdetdiaglem  22542  tsmsxp  24099  ustssco  24159  setsmstopn  24422  metustexhalf  24500  tngtopn  24594  equivcau  25256  metsscmetcld  25271  dvbssntr  25857  pserdv  26395  noseqrdgfn  28302  subgreldmiedg  29356  hlimcaui  31311  nfpconfp  32710  gsumfs2d  33144  symgcom2  33166  pmtrcnel  33171  pmtrcnel2  33172  pmtrcnelor  33173  cycpmrn  33225  metideq  34050  esum2d  34250  subgrwlk  35326  fundmpss  35961  fixssdm  36098  filnetlem3  36574  filnetlem4  36575  ssbnd  37989  bnd2lem  37992  ismrcd1  42940  istopclsd  42942  mptrcllem  43854  cnvrcl0  43866  dmtrcl  43868  dfrcl2  43915  relexpss1d  43946  rfovcnvf1od  44245  fourierdlem80  46430  issmflem  46971