Theorem dmss 5884

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 3925	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
2	1	eximdv 1950	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴 → ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵))
3		vex 3455	. . . 4 ⊢ 𝑥 ∈ V
4	3	eldm2 5883	. . 3 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
5	3	eldm2 5883	. . 3 ⊢ (𝑥 ∈ dom 𝐵 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵)
6	2, 4, 5	3imtr4g 299	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ dom 𝐴 → 𝑥 ∈ dom 𝐵))
7	6	ssrdv 3937	1 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)

This proof depends on syntax axioms:   → wi 4  ∃wex 1812   ∈ wcel 2145   ⊆ wss 3899  ⟨cop 4590  dom cdm 5651

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-dm 5661

This theorem is used by:  dmeq  5885  dmv  5904  rnss  5921  dmiin  5935  dmresss  6002  ssxpb  6165  sofld  6178  resssxp  6265  relrelss  6268  funssxp  6730  fndmdif  7033  fneqeql2  7038  dff3  7092  frxp  8127  fnwelem  8132  frxp2  8145  frxp3  8152  funsssuppss  8191  tposss  8228  frrlem8  8295  frrlem14  8301  smores  8344  smores2  8346  tfrlem13  8382  imafi  9291  hartogslem1  9520  wemapso  9529  dmttrcl  9706  r0weon  10072  infxpenlem  10073  brdom3  10588  brdom5  10589  brdom4  10590  fpwwe2lem12  10708  fpwwe2  10709  canth4  10713  canthwelem  10716  pwfseqlem4  10728  nqerf  10996  dmrecnq  11034  uzrdgfni  14081  hashdmpropge2  14608  dmtrclfv  15151  rlimpm  15647  isstruct2  17307  strleun  17315  imasaddfnlem  17680  imasvscafn  17689  isohom  17931  catcoppccl  18272  tsrss  18743  ledm  18744  dirdm  18754  f1omvdmvd  19637  mvdco  19639  f1omvdconj  19640  pmtrfb  19659  pmtrfconj  19660  symggen  19664  symggen2  19665  pmtrdifellem1  19670  pmtrdifellem2  19671  psgnunilem1  19687  gsum2d  20166  lspextmo  21311  dsmmfi  22024  lindfres  22109  mdetdiaglem  22893  tsmsxp  24454  ustssco  24514  setsmstopn  24777  metustexhalf  24855  tngtopn  24949  equivcau  25601  metsscmetcld  25616  dvbssntr  26200  pserdv  26738  noseqrdgfn  28674  subgreldmiedg  29846  subgrwlk  30251  hlimcaui  31820  nfpconfp  33208  gsumfs2d  33604  symgcom2  33627  pmtrcnel  33632  pmtrcnel2  33633  pmtrcnelor  33634  cycpmrn  33686  metideq  34507  esum2d  34707  fundmpss  36501  fixssdm  36638  filnetlem3  37138  filnetlem4  37139  ssbnd  38690  bnd2lem  38693  ismrcd1  43662  istopclsd  43664  mptrcllem  44572  cnvrcl0  44584  dmtrcl  44586  dfrcl2  44633  relexpss1d  44664  rfovcnvf1od  44963  fourierdlem80  47140  issmflem  47681