Theorem dmss 5859

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 3929	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
2	1	eximdv 1919	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴 → ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵))
3		vex 3446	. . . 4 ⊢ 𝑥 ∈ V
4	3	eldm2 5858	. . 3 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
5	3	eldm2 5858	. . 3 ⊢ (𝑥 ∈ dom 𝐵 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵)
6	2, 4, 5	3imtr4g 296	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ dom 𝐴 → 𝑥 ∈ dom 𝐵))
7	6	ssrdv 3941	1 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)

Syntax hints:   → wi 4  ∃wex 1781   ∈ wcel 2114   ⊆ wss 3903  ⟨cop 4588  dom cdm 5632

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-dm 5642

This theorem is referenced by:  dmeq  5860  dmv  5879  rnss  5896  dmiin  5910  dmresss  5978  ssxpb  6140  sofld  6153  resssxp  6236  relrelss  6239  funssxp  6698  fndmdif  6996  fneqeql2  7001  dff3  7054  frxp  8078  fnwelem  8083  frxp2  8096  frxp3  8103  funsssuppss  8142  tposss  8179  frrlem8  8245  frrlem14  8251  smores  8294  smores2  8296  tfrlem13  8331  imafi  9227  hartogslem1  9459  wemapso  9468  dmttrcl  9642  r0weon  9934  infxpenlem  9935  brdom3  10450  brdom5  10451  brdom4  10452  fpwwe2lem12  10565  fpwwe2  10566  canth4  10570  canthwelem  10573  pwfseqlem4  10585  nqerf  10853  dmrecnq  10891  uzrdgfni  13893  hashdmpropge2  14418  dmtrclfv  14953  rlimpm  15435  isstruct2  17088  strleun  17096  imasaddfnlem  17461  imasvscafn  17470  isohom  17712  catcoppccl  18053  tsrss  18524  ledm  18525  dirdm  18535  f1omvdmvd  19384  mvdco  19386  f1omvdconj  19387  pmtrfb  19406  pmtrfconj  19407  symggen  19411  symggen2  19412  pmtrdifellem1  19417  pmtrdifellem2  19418  psgnunilem1  19434  gsum2d  19913  lspextmo  21020  dsmmfi  21705  lindfres  21790  mdetdiaglem  22554  tsmsxp  24111  ustssco  24171  setsmstopn  24434  metustexhalf  24512  tngtopn  24606  equivcau  25268  metsscmetcld  25283  dvbssntr  25869  pserdv  26407  noseqrdgfn  28314  subgreldmiedg  29368  hlimcaui  31323  nfpconfp  32721  gsumfs2d  33154  symgcom2  33177  pmtrcnel  33182  pmtrcnel2  33183  pmtrcnelor  33184  cycpmrn  33236  metideq  34070  esum2d  34270  subgrwlk  35345  fundmpss  35980  fixssdm  36117  filnetlem3  36593  filnetlem4  36594  ssbnd  38036  bnd2lem  38039  ismrcd1  43052  istopclsd  43054  mptrcllem  43966  cnvrcl0  43978  dmtrcl  43980  dfrcl2  44027  relexpss1d  44058  rfovcnvf1od  44357  fourierdlem80  46541  issmflem  47082