Theorem dmss 5876

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 3930	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
2	1	eximdv 1936	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴 → ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵))
3		vex 3457	. . . 4 ⊢ 𝑥 ∈ V
4	3	eldm2 5875	. . 3 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
5	3	eldm2 5875	. . 3 ⊢ (𝑥 ∈ dom 𝐵 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵)
6	2, 4, 5	3imtr4g 298	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ dom 𝐴 → 𝑥 ∈ dom 𝐵))
7	6	ssrdv 3942	1 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)

Syntax hints:   → wi 4  ∃wex 1798   ∈ wcel 2141   ⊆ wss 3904  ⟨cop 4587  dom cdm 5645

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-dm 5655

This theorem is referenced by:  dmeq  5877  dmv  5896  rnss  5913  dmiin  5927  dmresss  5995  ssxpb  6156  sofld  6169  resssxp  6253  relrelss  6256  funssxp  6716  fndmdif  7019  fneqeql2  7024  dff3  7077  frxp  8101  fnwelem  8106  frxp2  8119  frxp3  8126  funsssuppss  8165  tposss  8202  frrlem8  8269  frrlem14  8275  smores  8318  smores2  8320  tfrlem13  8356  imafi  9255  hartogslem1  9487  wemapso  9496  dmttrcl  9673  r0weon  9965  infxpenlem  9966  brdom3  10482  brdom5  10483  brdom4  10484  fpwwe2lem12  10597  fpwwe2  10598  canth4  10602  canthwelem  10605  pwfseqlem4  10617  nqerf  10885  dmrecnq  10923  uzrdgfni  13968  hashdmpropge2  14493  dmtrclfv  15028  rlimpm  15510  isstruct2  17168  strleun  17176  imasaddfnlem  17541  imasvscafn  17550  isohom  17792  catcoppccl  18133  tsrss  18604  ledm  18605  dirdm  18615  f1omvdmvd  19466  mvdco  19468  f1omvdconj  19469  pmtrfb  19488  pmtrfconj  19489  symggen  19493  symggen2  19494  pmtrdifellem1  19499  pmtrdifellem2  19500  psgnunilem1  19516  gsum2d  19995  lspextmo  21103  dsmmfi  21770  lindfres  21855  mdetdiaglem  22638  tsmsxp  24195  ustssco  24255  setsmstopn  24518  metustexhalf  24596  tngtopn  24690  equivcau  25342  metsscmetcld  25357  dvbssntr  25942  pserdv  26469  noseqrdgfn  28376  subgreldmiedg  29430  hlimcaui  31385  nfpconfp  32784  gsumfs2d  33202  symgcom2  33225  pmtrcnel  33230  pmtrcnel2  33231  pmtrcnelor  33232  cycpmrn  33284  metideq  34151  esum2d  34351  subgrwlk  35446  fundmpss  36081  fixssdm  36218  filnetlem3  36704  filnetlem4  36705  ssbnd  38251  bnd2lem  38254  ismrcd1  43243  istopclsd  43245  mptrcllem  44153  cnvrcl0  44165  dmtrcl  44167  dfrcl2  44214  relexpss1d  44245  rfovcnvf1od  44544  fourierdlem80  46724  issmflem  47265