Theorem dmss 5868

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 3942	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
2	1	eximdv 1917	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴 → ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵))
3		vex 3454	. . . 4 ⊢ 𝑥 ∈ V
4	3	eldm2 5867	. . 3 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
5	3	eldm2 5867	. . 3 ⊢ (𝑥 ∈ dom 𝐵 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵)
6	2, 4, 5	3imtr4g 296	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ dom 𝐴 → 𝑥 ∈ dom 𝐵))
7	6	ssrdv 3954	1 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)

Syntax hints:   → wi 4  ∃wex 1779   ∈ wcel 2109   ⊆ wss 3916  ⟨cop 4597  dom cdm 5640

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3919  df-un 3921  df-ss 3933  df-nul 4299  df-if 4491  df-sn 4592  df-pr 4594  df-op 4598  df-br 5110  df-dm 5650

This theorem is referenced by:  dmeq  5869  dmv  5888  rnss  5905  dmiin  5919  dmresss  5984  ssxpb  6149  sofld  6162  resssxp  6245  relrelss  6248  funssxp  6718  fndmdif  7016  fneqeql2  7021  dff3  7074  frxp  8107  fnwelem  8112  frxp2  8125  frxp3  8132  funsssuppss  8171  tposss  8208  frrlem8  8274  frrlem14  8280  smores  8323  smores2  8325  tfrlem13  8360  imafi  9270  hartogslem1  9501  wemapso  9510  dmttrcl  9680  r0weon  9971  infxpenlem  9972  brdom3  10487  brdom5  10488  brdom4  10489  fpwwe2lem12  10601  fpwwe2  10602  canth4  10606  canthwelem  10609  pwfseqlem4  10621  nqerf  10889  dmrecnq  10927  uzrdgfni  13929  hashdmpropge2  14454  dmtrclfv  14990  rlimpm  15472  isstruct2  17125  strleun  17133  imasaddfnlem  17497  imasvscafn  17506  isohom  17744  catcoppccl  18085  tsrss  18554  ledm  18555  dirdm  18565  f1omvdmvd  19379  mvdco  19381  f1omvdconj  19382  pmtrfb  19401  pmtrfconj  19402  symggen  19406  symggen2  19407  pmtrdifellem1  19412  pmtrdifellem2  19413  psgnunilem1  19429  gsum2d  19908  lspextmo  20969  dsmmfi  21653  lindfres  21738  mdetdiaglem  22491  tsmsxp  24048  ustssco  24108  setsmstopn  24372  metustexhalf  24450  tngtopn  24544  equivcau  25206  metsscmetcld  25221  dvbssntr  25807  pserdv  26345  noseqrdgfn  28206  subgreldmiedg  29216  hlimcaui  31171  nfpconfp  32562  gsumfs2d  33001  symgcom2  33047  pmtrcnel  33052  pmtrcnel2  33053  pmtrcnelor  33054  cycpmrn  33106  metideq  33889  esum2d  34089  subgrwlk  35119  fundmpss  35749  fixssdm  35889  filnetlem3  36363  filnetlem4  36364  ssbnd  37777  bnd2lem  37780  ismrcd1  42679  istopclsd  42681  mptrcllem  43595  cnvrcl0  43607  dmtrcl  43609  dfrcl2  43656  relexpss1d  43687  rfovcnvf1od  43986  fourierdlem80  46177  issmflem  46718