Theorem dmss 5866

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

Syntax hints:   → wi 4  ∃wex 1779   ∈ wcel 2109   ⊆ wss 3914  ⟨cop 4595  dom cdm 5638

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-dm 5648

This theorem is referenced by:  dmeq  5867  dmv  5886  rnss  5903  dmiin  5917  dmresss  5982  ssxpb  6147  sofld  6160  resssxp  6243  relrelss  6246  funssxp  6716  fndmdif  7014  fneqeql2  7019  dff3  7072  frxp  8105  fnwelem  8110  frxp2  8123  frxp3  8130  funsssuppss  8169  tposss  8206  frrlem8  8272  frrlem14  8278  smores  8321  smores2  8323  tfrlem13  8358  imafi  9264  hartogslem1  9495  wemapso  9504  dmttrcl  9674  r0weon  9965  infxpenlem  9966  brdom3  10481  brdom5  10482  brdom4  10483  fpwwe2lem12  10595  fpwwe2  10596  canth4  10600  canthwelem  10603  pwfseqlem4  10615  nqerf  10883  dmrecnq  10921  uzrdgfni  13923  hashdmpropge2  14448  dmtrclfv  14984  rlimpm  15466  isstruct2  17119  strleun  17127  imasaddfnlem  17491  imasvscafn  17500  isohom  17738  catcoppccl  18079  tsrss  18548  ledm  18549  dirdm  18559  f1omvdmvd  19373  mvdco  19375  f1omvdconj  19376  pmtrfb  19395  pmtrfconj  19396  symggen  19400  symggen2  19401  pmtrdifellem1  19406  pmtrdifellem2  19407  psgnunilem1  19423  gsum2d  19902  lspextmo  20963  dsmmfi  21647  lindfres  21732  mdetdiaglem  22485  tsmsxp  24042  ustssco  24102  setsmstopn  24366  metustexhalf  24444  tngtopn  24538  equivcau  25200  metsscmetcld  25215  dvbssntr  25801  pserdv  26339  noseqrdgfn  28200  subgreldmiedg  29210  hlimcaui  31165  nfpconfp  32556  gsumfs2d  32995  symgcom2  33041  pmtrcnel  33046  pmtrcnel2  33047  pmtrcnelor  33048  cycpmrn  33100  metideq  33883  esum2d  34083  subgrwlk  35119  fundmpss  35754  fixssdm  35894  filnetlem3  36368  filnetlem4  36369  ssbnd  37782  bnd2lem  37785  ismrcd1  42686  istopclsd  42688  mptrcllem  43602  cnvrcl0  43614  dmtrcl  43616  dfrcl2  43663  relexpss1d  43694  rfovcnvf1od  43993  fourierdlem80  46184  issmflem  46725