Theorem dmss 5849

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

Syntax hints:   → wi 4  ∃wex 1779   ∈ wcel 2109   ⊆ wss 3905  ⟨cop 4585  dom cdm 5623

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 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-dm 5633

This theorem is referenced by:  dmeq  5850  dmv  5869  rnss  5885  dmiin  5899  dmresss  5966  ssxpb  6127  sofld  6140  resssxp  6222  relrelss  6225  funssxp  6684  fndmdif  6980  fneqeql2  6985  dff3  7038  frxp  8066  fnwelem  8071  frxp2  8084  frxp3  8091  funsssuppss  8130  tposss  8167  frrlem8  8233  frrlem14  8239  smores  8282  smores2  8284  tfrlem13  8319  imafi  9222  hartogslem1  9453  wemapso  9462  dmttrcl  9636  r0weon  9925  infxpenlem  9926  brdom3  10441  brdom5  10442  brdom4  10443  fpwwe2lem12  10555  fpwwe2  10556  canth4  10560  canthwelem  10563  pwfseqlem4  10575  nqerf  10843  dmrecnq  10881  uzrdgfni  13883  hashdmpropge2  14408  dmtrclfv  14943  rlimpm  15425  isstruct2  17078  strleun  17086  imasaddfnlem  17450  imasvscafn  17459  isohom  17701  catcoppccl  18042  tsrss  18513  ledm  18514  dirdm  18524  f1omvdmvd  19340  mvdco  19342  f1omvdconj  19343  pmtrfb  19362  pmtrfconj  19363  symggen  19367  symggen2  19368  pmtrdifellem1  19373  pmtrdifellem2  19374  psgnunilem1  19390  gsum2d  19869  lspextmo  20978  dsmmfi  21663  lindfres  21748  mdetdiaglem  22501  tsmsxp  24058  ustssco  24118  setsmstopn  24382  metustexhalf  24460  tngtopn  24554  equivcau  25216  metsscmetcld  25231  dvbssntr  25817  pserdv  26355  noseqrdgfn  28223  subgreldmiedg  29246  hlimcaui  31198  nfpconfp  32589  gsumfs2d  33021  symgcom2  33039  pmtrcnel  33044  pmtrcnel2  33045  pmtrcnelor  33046  cycpmrn  33098  metideq  33862  esum2d  34062  subgrwlk  35107  fundmpss  35742  fixssdm  35882  filnetlem3  36356  filnetlem4  36357  ssbnd  37770  bnd2lem  37773  ismrcd1  42674  istopclsd  42676  mptrcllem  43589  cnvrcl0  43601  dmtrcl  43603  dfrcl2  43650  relexpss1d  43681  rfovcnvf1od  43980  fourierdlem80  46171  issmflem  46712