Theorem dmss 5824

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

Syntax hints:   → wi 4  ∃wex 1779   ∈ wcel 2104   ⊆ wss 3892  ⟨cop 4571  dom cdm 5600

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3306  df-v 3439  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4566  df-pr 4568  df-op 4572  df-br 5082  df-dm 5610

This theorem is referenced by:  dmeq  5825  dmv  5844  rnss  5860  dmiin  5874  ssxpb  6092  sofld  6105  resssxp  6188  relrelss  6191  funssxp  6659  fndmdif  6951  fneqeql2  6956  dff3  7008  frxp  7998  fnwelem  8003  funsssuppss  8037  tposss  8074  frrlem8  8140  frrlem14  8146  wfrlem16OLD  8186  smores  8214  smores2  8216  tfrlem13  8252  imafiALT  9160  hartogslem1  9349  wemapso  9358  dmttrcl  9527  r0weon  9818  infxpenlem  9819  brdom3  10334  brdom5  10335  brdom4  10336  fpwwe2lem12  10448  fpwwe2  10449  canth4  10453  canthwelem  10456  pwfseqlem4  10468  nqerf  10736  dmrecnq  10774  uzrdgfni  13728  hashdmpropge2  14246  dmtrclfv  14778  rlimpm  15258  isstruct2  16899  strleun  16907  imasaddfnlem  17288  imasvscafn  17297  isohom  17537  catcoppccl  17881  catcoppcclOLD  17882  tsrss  18356  ledm  18357  dirdm  18367  f1omvdmvd  19100  mvdco  19102  f1omvdconj  19103  pmtrfb  19122  pmtrfconj  19123  symggen  19127  symggen2  19128  pmtrdifellem1  19133  pmtrdifellem2  19134  psgnunilem1  19150  gsum2d  19622  lspextmo  20367  dsmmfi  20994  lindfres  21079  mdetdiaglem  21796  tsmsxp  23355  ustssco  23415  setsmstopn  23682  metustexhalf  23761  tngtopn  23863  equivcau  24513  metsscmetcld  24528  dvbssntr  25113  pserdv  25637  subgreldmiedg  27699  hlimcaui  29647  nfpconfp  31016  symgcom2  31402  pmtrcnel  31407  pmtrcnel2  31408  pmtrcnelor  31409  cycpmrn  31459  metideq  31892  esum2d  32110  subgrwlk  33143  fundmpss  33789  frxp2  33840  frxp3  33846  fixssdm  34257  filnetlem3  34618  filnetlem4  34619  ssbnd  35994  bnd2lem  35997  ismrcd1  40715  istopclsd  40717  mptrcllem  41434  cnvrcl0  41446  dmtrcl  41448  dfrcl2  41495  relexpss1d  41526  rfovcnvf1od  41825  fourierdlem80  43956  issmflem  44495