Theorem dmss 5851

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 3916	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
2	1	eximdv 1924	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴 → ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵))
3		vex 3436	. . . 4 ⊢ 𝑥 ∈ V
4	3	eldm2 5850	. . 3 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
5	3	eldm2 5850	. . 3 ⊢ (𝑥 ∈ dom 𝐵 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵)
6	2, 4, 5	3imtr4g 297	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ dom 𝐴 → 𝑥 ∈ dom 𝐵))
7	6	ssrdv 3928	1 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)

Syntax hints:   → wi 4  ∃wex 1786   ∈ wcel 2119   ⊆ wss 3890  ⟨cop 4568  dom cdm 5625

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 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-dm 5635

This theorem is referenced by:  dmeq  5852  dmv  5871  rnss  5888  dmiin  5902  dmresss  5970  ssxpb  6132  sofld  6145  resssxp  6228  relrelss  6231  funssxp  6690  fndmdif  6990  fneqeql2  6995  dff3  7048  frxp  8073  fnwelem  8078  frxp2  8091  frxp3  8098  funsssuppss  8137  tposss  8174  frrlem8  8240  frrlem14  8246  smores  8289  smores2  8291  tfrlem13  8326  imafi  9222  hartogslem1  9454  wemapso  9463  dmttrcl  9640  r0weon  9932  infxpenlem  9933  brdom3  10448  brdom5  10449  brdom4  10450  fpwwe2lem12  10563  fpwwe2  10564  canth4  10568  canthwelem  10571  pwfseqlem4  10583  nqerf  10851  dmrecnq  10889  uzrdgfni  13918  hashdmpropge2  14443  dmtrclfv  14978  rlimpm  15460  isstruct2  17117  strleun  17125  imasaddfnlem  17490  imasvscafn  17499  isohom  17741  catcoppccl  18082  tsrss  18553  ledm  18554  dirdm  18564  f1omvdmvd  19416  mvdco  19418  f1omvdconj  19419  pmtrfb  19438  pmtrfconj  19439  symggen  19443  symggen2  19444  pmtrdifellem1  19449  pmtrdifellem2  19450  psgnunilem1  19466  gsum2d  19945  lspextmo  21053  dsmmfi  21720  lindfres  21805  mdetdiaglem  22588  tsmsxp  24145  ustssco  24205  setsmstopn  24468  metustexhalf  24546  tngtopn  24640  equivcau  25292  metsscmetcld  25307  dvbssntr  25892  pserdv  26419  noseqrdgfn  28323  subgreldmiedg  29377  hlimcaui  31332  nfpconfp  32731  gsumfs2d  33149  symgcom2  33172  pmtrcnel  33177  pmtrcnel2  33178  pmtrcnelor  33179  cycpmrn  33231  metideq  34084  esum2d  34284  subgrwlk  35367  fundmpss  36002  fixssdm  36139  filnetlem3  36615  filnetlem4  36616  ssbnd  38162  bnd2lem  38165  ismrcd1  43154  istopclsd  43156  mptrcllem  44064  cnvrcl0  44076  dmtrcl  44078  dfrcl2  44125  relexpss1d  44156  rfovcnvf1od  44455  fourierdlem80  46636  issmflem  47177