Theorem dmss 5890

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

This proof depends on syntax axioms:   → wi 4  ∃wex 1812   ∈ wcel 2145   ⊆ wss 3902  ⟨cop 4593  dom cdm 5659

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 2147  ax-9 2155  ax-ext 2734

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 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-dm 5669

This theorem is used by:  dmeq  5891  dmv  5910  rnss  5927  dmiin  5941  dmresss  6008  ssxpb  6171  sofld  6184  resssxp  6271  relrelss  6274  funssxp  6735  fndmdif  7038  fneqeql2  7043  dff3  7097  frxp  8128  fnwelem  8133  frxp2  8146  frxp3  8153  funsssuppss  8192  tposss  8229  frrlem8  8296  frrlem14  8302  smores  8345  smores2  8347  tfrlem13  8383  imafi  9289  hartogslem1  9518  wemapso  9527  dmttrcl  9704  r0weon  10019  infxpenlem  10020  brdom3  10535  brdom5  10536  brdom4  10537  fpwwe2lem12  10655  fpwwe2  10656  canth4  10660  canthwelem  10663  pwfseqlem4  10675  nqerf  10943  dmrecnq  10981  uzrdgfni  14026  hashdmpropge2  14552  dmtrclfv  15095  rlimpm  15591  isstruct2  17247  strleun  17255  imasaddfnlem  17620  imasvscafn  17629  isohom  17871  catcoppccl  18212  tsrss  18683  ledm  18684  dirdm  18694  f1omvdmvd  19576  mvdco  19578  f1omvdconj  19579  pmtrfb  19598  pmtrfconj  19599  symggen  19603  symggen2  19604  pmtrdifellem1  19609  pmtrdifellem2  19610  psgnunilem1  19626  gsum2d  20105  lspextmo  21246  dsmmfi  21957  lindfres  22042  mdetdiaglem  22826  tsmsxp  24387  ustssco  24447  setsmstopn  24710  metustexhalf  24788  tngtopn  24882  equivcau  25534  metsscmetcld  25549  dvbssntr  26134  pserdv  26672  noseqrdgfn  28579  subgreldmiedg  29751  subgrwlk  30156  hlimcaui  31725  nfpconfp  33113  gsumfs2d  33509  symgcom2  33532  pmtrcnel  33537  pmtrcnel2  33538  pmtrcnelor  33539  cycpmrn  33591  metideq  34411  esum2d  34611  fundmpss  36354  fixssdm  36491  filnetlem3  37007  filnetlem4  37008  ssbnd  38546  bnd2lem  38549  ismrcd1  43551  istopclsd  43553  mptrcllem  44461  cnvrcl0  44473  dmtrcl  44475  dfrcl2  44522  relexpss1d  44553  rfovcnvf1od  44852  fourierdlem80  47022  issmflem  47563