Theorem dmss 5842

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

Syntax hints:   → wi 4  ∃wex 1780   ∈ wcel 2111   ⊆ wss 3902  ⟨cop 4582  dom cdm 5616

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-br 5092  df-dm 5626

This theorem is referenced by:  dmeq  5843  dmv  5862  rnss  5879  dmiin  5893  dmresss  5960  ssxpb  6121  sofld  6134  resssxp  6217  relrelss  6220  funssxp  6679  fndmdif  6975  fneqeql2  6980  dff3  7033  frxp  8056  fnwelem  8061  frxp2  8074  frxp3  8081  funsssuppss  8120  tposss  8157  frrlem8  8223  frrlem14  8229  smores  8272  smores2  8274  tfrlem13  8309  imafi  9199  hartogslem1  9428  wemapso  9437  dmttrcl  9611  r0weon  9903  infxpenlem  9904  brdom3  10419  brdom5  10420  brdom4  10421  fpwwe2lem12  10533  fpwwe2  10534  canth4  10538  canthwelem  10541  pwfseqlem4  10553  nqerf  10821  dmrecnq  10859  uzrdgfni  13865  hashdmpropge2  14390  dmtrclfv  14925  rlimpm  15407  isstruct2  17060  strleun  17068  imasaddfnlem  17432  imasvscafn  17441  isohom  17683  catcoppccl  18024  tsrss  18495  ledm  18496  dirdm  18506  f1omvdmvd  19356  mvdco  19358  f1omvdconj  19359  pmtrfb  19378  pmtrfconj  19379  symggen  19383  symggen2  19384  pmtrdifellem1  19389  pmtrdifellem2  19390  psgnunilem1  19406  gsum2d  19885  lspextmo  20991  dsmmfi  21676  lindfres  21761  mdetdiaglem  22514  tsmsxp  24071  ustssco  24131  setsmstopn  24394  metustexhalf  24472  tngtopn  24566  equivcau  25228  metsscmetcld  25243  dvbssntr  25829  pserdv  26367  noseqrdgfn  28237  subgreldmiedg  29262  hlimcaui  31214  nfpconfp  32612  gsumfs2d  33033  symgcom2  33051  pmtrcnel  33056  pmtrcnel2  33057  pmtrcnelor  33058  cycpmrn  33110  metideq  33904  esum2d  34104  subgrwlk  35174  fundmpss  35809  fixssdm  35946  filnetlem3  36420  filnetlem4  36421  ssbnd  37834  bnd2lem  37837  ismrcd1  42737  istopclsd  42739  mptrcllem  43652  cnvrcl0  43664  dmtrcl  43666  dfrcl2  43713  relexpss1d  43744  rfovcnvf1od  44043  fourierdlem80  46230  issmflem  46771