Theorem dmss 5892

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 3907	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
2	1	eximdv 1952	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴 → ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵))
3		vex 3458	. . . 4 ⊢ 𝑥 ∈ V
4	3	eldm2 5891	. . 3 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
5	3	eldm2 5891	. . 3 ⊢ (𝑥 ∈ dom 𝐵 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵)
6	2, 4, 5	3imtr4g 299	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ dom 𝐴 → 𝑥 ∈ dom 𝐵))
7	6	ssrdv 3919	1 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)

This proof depends on syntax axioms:   → wi 4  ∃wex 1812   ∈ wcel 2147   ⊆ wss 3900  ⟨cop 4838  dom cdm 5656

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-dm 5666

This theorem is used by:  dmeq  5893  dmv  5912  rnss  5929  dmiin  5943  dmresss  6015  ssxpb  6179  sofld  6192  resssxp  6291  relrelss  6294  funssxp  6763  fndmdif  7067  fneqeql2  7072  dff3  7127  frxp  8168  fnwelem  8173  frxp2  8191  frxp3  8198  funsssuppss  8238  tposss  8275  frrlem8  8342  frrlem14  8348  smores2  8393  tfrlem13  8429  imafi  9338  hartogslem1  9566  wemapso  9575  dmttrcl  9752  r0weon  10121  infxpenlem  10122  brdom3  10637  brdom5  10638  brdom4  10639  fpwwe2lem12  10757  fpwwe2  10758  canth4  10762  canthwelem  10765  pwfseqlem4  10777  nqerf  11045  dmrecnq  11083  uzrdgfni  14131  hashdmpropge2  14658  dmtrclfv  15203  rlimpm  15699  isstruct2  17359  strleun  17367  imasaddfnlem  17732  imasvscafn  17741  isohom  17983  catcoppccl  18324  tsrss  18795  ledm  18796  dirdm  18806  f1omvdmvd  19690  mvdco  19692  f1omvdconj  19693  pmtrfb  19712  pmtrfconj  19713  symggen  19717  symggen2  19718  pmtrdifellem1  19723  pmtrdifellem2  19724  psgnunilem1  19740  gsum2d  20219  lspextmo  21364  dsmmfi  22077  lindfres  22162  mdetdiaglem  22946  tsmsxp  24507  ustssco  24567  setsmstopn  24830  metustexhalf  24908  tngtopn  25002  equivcau  25654  metsscmetcld  25669  dvbssntr  26253  pserdv  26789  noseqrdgfn  28725  subgreldmiedg  29897  subgrwlk  30302  hlimcaui  31871  nfpconfp  33301  gsumfs2d  33698  symgcom2  33721  pmtrcnel  33726  pmtrcnel2  33727  pmtrcnelor  33728  cycpmrn  33780  metideq  34608  esum2d  34808  fundmpss  36723  fixssdm  36859  filnetlem3  37359  filnetlem4  37360  ssbnd  38925  bnd2lem  38928  ismrcd1  43913  istopclsd  43915  mptrcllem  44816  cnvrcl0  44828  dmtrcl  44830  dfrcl2  44877  relexpss1d  44908  rfovcnvf1od  45207  fourierdlem80  47411  issmflem  47952