Theorem dmss 5903

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 1921	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴 → ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵))
3		vex 3479	. . . 4 ⊢ 𝑥 ∈ V
4	3	eldm2 5902	. . 3 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
5	3	eldm2 5902	. . 3 ⊢ (𝑥 ∈ dom 𝐵 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵)
6	2, 4, 5	3imtr4g 296	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ dom 𝐴 → 𝑥 ∈ dom 𝐵))
7	6	ssrdv 3989	1 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)

Syntax hints:   → wi 4  ∃wex 1782   ∈ wcel 2107   ⊆ wss 3949  ⟨cop 4635  dom cdm 5677

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-dm 5687

This theorem is referenced by:  dmeq  5904  dmv  5923  rnss  5939  dmiin  5953  ssxpb  6174  sofld  6187  resssxp  6270  relrelss  6273  funssxp  6747  fndmdif  7044  fneqeql2  7049  dff3  7102  frxp  8112  fnwelem  8117  frxp2  8130  frxp3  8137  funsssuppss  8175  tposss  8212  frrlem8  8278  frrlem14  8284  wfrlem16OLD  8324  smores  8352  smores2  8354  tfrlem13  8390  imafiALT  9345  hartogslem1  9537  wemapso  9546  dmttrcl  9716  r0weon  10007  infxpenlem  10008  brdom3  10523  brdom5  10524  brdom4  10525  fpwwe2lem12  10637  fpwwe2  10638  canth4  10642  canthwelem  10645  pwfseqlem4  10657  nqerf  10925  dmrecnq  10963  uzrdgfni  13923  hashdmpropge2  14444  dmtrclfv  14965  rlimpm  15444  isstruct2  17082  strleun  17090  imasaddfnlem  17474  imasvscafn  17483  isohom  17723  catcoppccl  18067  catcoppcclOLD  18068  tsrss  18542  ledm  18543  dirdm  18553  f1omvdmvd  19311  mvdco  19313  f1omvdconj  19314  pmtrfb  19333  pmtrfconj  19334  symggen  19338  symggen2  19339  pmtrdifellem1  19344  pmtrdifellem2  19345  psgnunilem1  19361  gsum2d  19840  lspextmo  20667  dsmmfi  21293  lindfres  21378  mdetdiaglem  22100  tsmsxp  23659  ustssco  23719  setsmstopn  23986  metustexhalf  24065  tngtopn  24167  equivcau  24817  metsscmetcld  24832  dvbssntr  25417  pserdv  25941  subgreldmiedg  28540  hlimcaui  30489  nfpconfp  31856  symgcom2  32245  pmtrcnel  32250  pmtrcnel2  32251  pmtrcnelor  32252  cycpmrn  32302  metideq  32873  esum2d  33091  subgrwlk  34123  fundmpss  34738  fixssdm  34878  filnetlem3  35265  filnetlem4  35266  ssbnd  36656  bnd2lem  36659  ismrcd1  41436  istopclsd  41438  mptrcllem  42364  cnvrcl0  42376  dmtrcl  42378  dfrcl2  42425  relexpss1d  42456  rfovcnvf1od  42755  fourierdlem80  44902  issmflem  45443