Theorem dmss 5927

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 5926	. . 3 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
5	3	eldm2 5926	. . 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 5700

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 5167  df-dm 5710

This theorem is referenced by:  dmeq  5928  dmv  5947  rnss  5964  dmiin  5978  dmresss  6040  ssxpb  6205  sofld  6218  resssxp  6301  relrelss  6304  funssxp  6776  fndmdif  7075  fneqeql2  7080  dff3  7134  frxp  8167  fnwelem  8172  frxp2  8185  frxp3  8192  funsssuppss  8231  tposss  8268  frrlem8  8334  frrlem14  8340  wfrlem16OLD  8380  smores  8408  smores2  8410  tfrlem13  8446  imafi  9381  hartogslem1  9611  wemapso  9620  dmttrcl  9790  r0weon  10081  infxpenlem  10082  brdom3  10597  brdom5  10598  brdom4  10599  fpwwe2lem12  10711  fpwwe2  10712  canth4  10716  canthwelem  10719  pwfseqlem4  10731  nqerf  10999  dmrecnq  11037  uzrdgfni  14009  hashdmpropge2  14532  dmtrclfv  15067  rlimpm  15546  isstruct2  17196  strleun  17204  imasaddfnlem  17588  imasvscafn  17597  isohom  17837  catcoppccl  18184  catcoppcclOLD  18185  tsrss  18659  ledm  18660  dirdm  18670  f1omvdmvd  19485  mvdco  19487  f1omvdconj  19488  pmtrfb  19507  pmtrfconj  19508  symggen  19512  symggen2  19513  pmtrdifellem1  19518  pmtrdifellem2  19519  psgnunilem1  19535  gsum2d  20014  lspextmo  21078  dsmmfi  21781  lindfres  21866  mdetdiaglem  22625  tsmsxp  24184  ustssco  24244  setsmstopn  24511  metustexhalf  24590  tngtopn  24692  equivcau  25353  metsscmetcld  25368  dvbssntr  25955  pserdv  26491  noseqrdgfn  28330  subgreldmiedg  29318  hlimcaui  31268  nfpconfp  32651  symgcom2  33077  pmtrcnel  33082  pmtrcnel2  33083  pmtrcnelor  33084  cycpmrn  33136  metideq  33839  esum2d  34057  subgrwlk  35100  fundmpss  35730  fixssdm  35870  filnetlem3  36346  filnetlem4  36347  ssbnd  37748  bnd2lem  37751  ismrcd1  42654  istopclsd  42656  mptrcllem  43575  cnvrcl0  43587  dmtrcl  43589  dfrcl2  43636  relexpss1d  43667  rfovcnvf1od  43966  fourierdlem80  46107  issmflem  46648