Theorem dmss 5928

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 4002	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
2	1	eximdv 1916	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴 → ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵))
3		vex 3492	. . . 4 ⊢ 𝑥 ∈ V
4	3	eldm2 5927	. . 3 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
5	3	eldm2 5927	. . 3 ⊢ (𝑥 ∈ dom 𝐵 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵)
6	2, 4, 5	3imtr4g 296	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ dom 𝐴 → 𝑥 ∈ dom 𝐵))
7	6	ssrdv 4014	1 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)

Syntax hints:   → wi 4  ∃wex 1777   ∈ wcel 2108   ⊆ wss 3976  ⟨cop 4654  dom cdm 5701

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5168  df-dm 5711

This theorem is referenced by:  dmeq  5929  dmv  5948  rnss  5965  dmiin  5979  dmresss  6043  ssxpb  6208  sofld  6221  resssxp  6304  relrelss  6307  funssxp  6779  fndmdif  7078  fneqeql2  7083  dff3  7137  frxp  8170  fnwelem  8175  frxp2  8188  frxp3  8195  funsssuppss  8234  tposss  8271  frrlem8  8337  frrlem14  8343  wfrlem16OLD  8383  smores  8411  smores2  8413  tfrlem13  8449  imafi  9384  hartogslem1  9614  wemapso  9623  dmttrcl  9793  r0weon  10084  infxpenlem  10085  brdom3  10600  brdom5  10601  brdom4  10602  fpwwe2lem12  10714  fpwwe2  10715  canth4  10719  canthwelem  10722  pwfseqlem4  10734  nqerf  11002  dmrecnq  11040  uzrdgfni  14026  hashdmpropge2  14549  dmtrclfv  15084  rlimpm  15563  isstruct2  17216  strleun  17224  imasaddfnlem  17608  imasvscafn  17617  isohom  17857  catcoppccl  18204  catcoppcclOLD  18205  tsrss  18679  ledm  18680  dirdm  18690  f1omvdmvd  19505  mvdco  19507  f1omvdconj  19508  pmtrfb  19527  pmtrfconj  19528  symggen  19532  symggen2  19533  pmtrdifellem1  19538  pmtrdifellem2  19539  psgnunilem1  19555  gsum2d  20034  lspextmo  21098  dsmmfi  21801  lindfres  21886  mdetdiaglem  22645  tsmsxp  24204  ustssco  24264  setsmstopn  24531  metustexhalf  24610  tngtopn  24712  equivcau  25373  metsscmetcld  25388  dvbssntr  25975  pserdv  26511  noseqrdgfn  28350  subgreldmiedg  29338  hlimcaui  31288  nfpconfp  32671  symgcom2  33097  pmtrcnel  33102  pmtrcnel2  33103  pmtrcnelor  33104  cycpmrn  33156  metideq  33859  esum2d  34077  subgrwlk  35120  fundmpss  35750  fixssdm  35890  filnetlem3  36366  filnetlem4  36367  ssbnd  37768  bnd2lem  37771  ismrcd1  42673  istopclsd  42675  mptrcllem  43594  cnvrcl0  43606  dmtrcl  43608  dfrcl2  43655  relexpss1d  43686  rfovcnvf1od  43985  fourierdlem80  46125  issmflem  46666