Theorem dmss 5735

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 3908	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
2	1	eximdv 1918	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴 → ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵))
3		vex 3444	. . . 4 ⊢ 𝑥 ∈ V
4	3	eldm2 5734	. . 3 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
5	3	eldm2 5734	. . 3 ⊢ (𝑥 ∈ dom 𝐵 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵)
6	2, 4, 5	3imtr4g 299	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ dom 𝐴 → 𝑥 ∈ dom 𝐵))
7	6	ssrdv 3921	1 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)

Syntax hints:   → wi 4  ∃wex 1781   ∈ wcel 2111   ⊆ wss 3881  ⟨cop 4531  dom cdm 5519

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-dm 5529

This theorem is referenced by:  dmeq  5736  dmv  5756  rnss  5773  dmiin  5789  ssxpb  5998  sofld  6011  resssxp  6089  relrelss  6092  funssxp  6509  fndmdif  6789  fneqeql2  6794  dff3  6843  frxp  7803  fnwelem  7808  funsssuppss  7839  tposss  7876  wfrlem16  7953  smores  7972  smores2  7974  tfrlem13  8009  imafi  8801  hartogslem1  8990  wemapso  8999  r0weon  9423  infxpenlem  9424  brdom3  9939  brdom5  9940  brdom4  9941  fpwwe2lem13  10053  fpwwe2  10054  canth4  10058  canthwelem  10061  pwfseqlem4  10073  nqerf  10341  dmrecnq  10379  uzrdgfni  13321  hashdmpropge2  13837  dmtrclfv  14369  rlimpm  14849  isstruct2  16485  strleun  16583  imasaddfnlem  16793  imasvscafn  16802  isohom  17038  catcoppccl  17360  tsrss  17825  ledm  17826  dirdm  17836  f1omvdmvd  18563  mvdco  18565  f1omvdconj  18566  pmtrfb  18585  pmtrfconj  18586  symggen  18590  symggen2  18591  pmtrdifellem1  18596  pmtrdifellem2  18597  psgnunilem1  18613  gsum2d  19085  lspextmo  19821  dsmmfi  20427  lindfres  20512  mdetdiaglem  21203  tsmsxp  22760  ustssco  22820  setsmstopn  23085  metustexhalf  23163  tngtopn  23256  equivcau  23904  metsscmetcld  23919  dvbssntr  24503  pserdv  25024  subgreldmiedg  27073  hlimcaui  29019  nfpconfp  30391  symgcom2  30778  pmtrcnel  30783  pmtrcnel2  30784  pmtrcnelor  30785  cycpmrn  30835  metideq  31246  esum2d  31462  subgrwlk  32492  fundmpss  33122  frrlem8  33243  frrlem14  33249  fixssdm  33480  filnetlem3  33841  filnetlem4  33842  ssbnd  35226  bnd2lem  35229  ismrcd1  39639  istopclsd  39641  mptrcllem  40313  cnvrcl0  40325  dmtrcl  40327  dfrcl2  40375  relexpss1d  40406  rfovcnvf1od  40705  fourierdlem80  42828  issmflem  43361