Theorem dmss 5897

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 3934	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
2	1	eximdv 1950	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴 → ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵))
3		vex 3462	. . . 4 ⊢ 𝑥 ∈ V
4	3	eldm2 5896	. . 3 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
5	3	eldm2 5896	. . 3 ⊢ (𝑥 ∈ dom 𝐵 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵)
6	2, 4, 5	3imtr4g 299	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ dom 𝐴 → 𝑥 ∈ dom 𝐵))
7	6	ssrdv 3946	1 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)

This proof depends on syntax axioms:   → wi 4  ∃wex 1812   ∈ wcel 2146   ⊆ wss 3908  ⟨cop 4600  dom cdm 5666

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

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 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5115  df-dm 5676

This theorem is used by:  dmeq  5898  dmv  5917  rnss  5934  dmiin  5948  dmresss  6015  ssxpb  6177  sofld  6190  resssxp  6277  relrelss  6280  funssxp  6741  fndmdif  7044  fneqeql2  7049  dff3  7102  frxp  8131  fnwelem  8136  frxp2  8149  frxp3  8156  funsssuppss  8195  tposss  8232  frrlem8  8299  frrlem14  8305  smores  8348  smores2  8350  tfrlem13  8386  imafi  9285  hartogslem1  9514  wemapso  9523  dmttrcl  9700  r0weon  10015  infxpenlem  10016  brdom3  10530  brdom5  10531  brdom4  10532  fpwwe2lem12  10645  fpwwe2  10646  canth4  10650  canthwelem  10653  pwfseqlem4  10665  nqerf  10933  dmrecnq  10971  uzrdgfni  14014  hashdmpropge2  14540  dmtrclfv  15081  rlimpm  15577  isstruct2  17234  strleun  17242  imasaddfnlem  17607  imasvscafn  17616  isohom  17858  catcoppccl  18199  tsrss  18670  ledm  18671  dirdm  18681  f1omvdmvd  19544  mvdco  19546  f1omvdconj  19547  pmtrfb  19566  pmtrfconj  19567  symggen  19571  symggen2  19572  pmtrdifellem1  19577  pmtrdifellem2  19578  psgnunilem1  19594  gsum2d  20073  lspextmo  21214  dsmmfi  21925  lindfres  22010  mdetdiaglem  22792  tsmsxp  24349  ustssco  24409  setsmstopn  24672  metustexhalf  24750  tngtopn  24844  equivcau  25496  metsscmetcld  25511  dvbssntr  26096  pserdv  26629  noseqrdgfn  28536  subgreldmiedg  29670  hlimcaui  31625  nfpconfp  33014  gsumfs2d  33412  symgcom2  33435  pmtrcnel  33440  pmtrcnel2  33441  pmtrcnelor  33442  cycpmrn  33494  metideq  34314  esum2d  34514  subgrwlk  35645  fundmpss  36280  fixssdm  36417  filnetlem3  36932  filnetlem4  36933  ssbnd  38480  bnd2lem  38483  ismrcd1  43470  istopclsd  43472  mptrcllem  44380  cnvrcl0  44392  dmtrcl  44394  dfrcl2  44441  relexpss1d  44472  rfovcnvf1od  44771  fourierdlem80  46941  issmflem  47482