Theorem dmss 5879

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

Syntax hints:   → wi 4  ∃wex 1778   ∈ wcel 2107   ⊆ wss 3924  ⟨cop 4605  dom cdm 5651

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3414  df-v 3459  df-dif 3927  df-un 3929  df-ss 3941  df-nul 4307  df-if 4499  df-sn 4600  df-pr 4602  df-op 4606  df-br 5117  df-dm 5661

This theorem is referenced by:  dmeq  5880  dmv  5899  rnss  5916  dmiin  5930  dmresss  5995  ssxpb  6160  sofld  6173  resssxp  6256  relrelss  6259  funssxp  6730  fndmdif  7028  fneqeql2  7033  dff3  7086  frxp  8119  fnwelem  8124  frxp2  8137  frxp3  8144  funsssuppss  8183  tposss  8220  frrlem8  8286  frrlem14  8292  wfrlem16OLD  8332  smores  8360  smores2  8362  tfrlem13  8398  imafi  9319  hartogslem1  9548  wemapso  9557  dmttrcl  9727  r0weon  10018  infxpenlem  10019  brdom3  10534  brdom5  10535  brdom4  10536  fpwwe2lem12  10648  fpwwe2  10649  canth4  10653  canthwelem  10656  pwfseqlem4  10668  nqerf  10936  dmrecnq  10974  uzrdgfni  13965  hashdmpropge2  14489  dmtrclfv  15024  rlimpm  15503  isstruct2  17153  strleun  17161  imasaddfnlem  17527  imasvscafn  17536  isohom  17774  catcoppccl  18115  tsrss  18584  ledm  18585  dirdm  18595  f1omvdmvd  19409  mvdco  19411  f1omvdconj  19412  pmtrfb  19431  pmtrfconj  19432  symggen  19436  symggen2  19437  pmtrdifellem1  19442  pmtrdifellem2  19443  psgnunilem1  19459  gsum2d  19938  lspextmo  20999  dsmmfi  21683  lindfres  21768  mdetdiaglem  22521  tsmsxp  24078  ustssco  24138  setsmstopn  24402  metustexhalf  24480  tngtopn  24574  equivcau  25237  metsscmetcld  25252  dvbssntr  25838  pserdv  26376  noseqrdgfn  28215  subgreldmiedg  29194  hlimcaui  31149  nfpconfp  32543  gsumfs2d  32967  symgcom2  33013  pmtrcnel  33018  pmtrcnel2  33019  pmtrcnelor  33020  cycpmrn  33072  metideq  33832  esum2d  34032  subgrwlk  35075  fundmpss  35705  fixssdm  35845  filnetlem3  36319  filnetlem4  36320  ssbnd  37733  bnd2lem  37736  ismrcd1  42646  istopclsd  42648  mptrcllem  43562  cnvrcl0  43574  dmtrcl  43576  dfrcl2  43623  relexpss1d  43654  rfovcnvf1od  43953  fourierdlem80  46145  issmflem  46686