Theorem dmss 5739

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 3868	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
2	1	eximdv 1923	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴 → ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵))
3		vex 3401	. . . 4 ⊢ 𝑥 ∈ V
4	3	eldm2 5738	. . 3 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
5	3	eldm2 5738	. . 3 ⊢ (𝑥 ∈ dom 𝐵 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵)
6	2, 4, 5	3imtr4g 299	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ dom 𝐴 → 𝑥 ∈ dom 𝐵))
7	6	ssrdv 3881	1 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)

Syntax hints:   → wi 4  ∃wex 1786   ∈ wcel 2113   ⊆ wss 3841  ⟨cop 4519  dom cdm 5519

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3399  df-un 3846  df-in 3848  df-ss 3858  df-sn 4514  df-pr 4516  df-op 4520  df-br 5028  df-dm 5529

This theorem is referenced by:  dmeq  5740  dmv  5759  rnss  5776  dmiin  5790  ssxpb  6000  sofld  6013  resssxp  6096  relrelss  6099  funssxp  6527  fndmdif  6813  fneqeql2  6818  dff3  6870  frxp  7839  fnwelem  7844  funsssuppss  7878  tposss  7915  wfrlem16  7992  smores  8011  smores2  8013  tfrlem13  8048  imafiOLD  8883  hartogslem1  9072  wemapso  9081  r0weon  9505  infxpenlem  9506  brdom3  10021  brdom5  10022  brdom4  10023  fpwwe2lem12  10135  fpwwe2  10136  canth4  10140  canthwelem  10143  pwfseqlem4  10155  nqerf  10423  dmrecnq  10461  uzrdgfni  13410  hashdmpropge2  13928  dmtrclfv  14460  rlimpm  14940  isstruct2  16589  strleun  16687  imasaddfnlem  16897  imasvscafn  16906  isohom  17144  catcoppccl  17477  tsrss  17942  ledm  17943  dirdm  17953  f1omvdmvd  18682  mvdco  18684  f1omvdconj  18685  pmtrfb  18704  pmtrfconj  18705  symggen  18709  symggen2  18710  pmtrdifellem1  18715  pmtrdifellem2  18716  psgnunilem1  18732  gsum2d  19204  lspextmo  19940  dsmmfi  20547  lindfres  20632  mdetdiaglem  21342  tsmsxp  22899  ustssco  22959  setsmstopn  23224  metustexhalf  23302  tngtopn  23396  equivcau  24045  metsscmetcld  24060  dvbssntr  24644  pserdv  25168  subgreldmiedg  27217  hlimcaui  29163  nfpconfp  30533  symgcom2  30922  pmtrcnel  30927  pmtrcnel2  30928  pmtrcnelor  30929  cycpmrn  30979  metideq  31407  esum2d  31623  subgrwlk  32657  fundmpss  33304  frxp2  33394  frxp3  33400  frrlem8  33440  frrlem14  33446  fixssdm  33838  filnetlem3  34199  filnetlem4  34200  ssbnd  35558  bnd2lem  35561  ismrcd1  40076  istopclsd  40078  mptrcllem  40750  cnvrcl0  40762  dmtrcl  40764  dfrcl2  40812  relexpss1d  40843  rfovcnvf1od  41142  fourierdlem80  43253  issmflem  43786