Theorem dmss 5902

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

Syntax hints:   → wi 4  ∃wex 1780   ∈ wcel 2105   ⊆ wss 3948  ⟨cop 4634  dom cdm 5676

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-dm 5686

This theorem is referenced by:  dmeq  5903  dmv  5922  rnss  5938  dmiin  5952  ssxpb  6173  sofld  6186  resssxp  6269  relrelss  6272  funssxp  6746  fndmdif  7043  fneqeql2  7048  dff3  7101  frxp  8117  fnwelem  8122  frxp2  8135  frxp3  8142  funsssuppss  8180  tposss  8218  frrlem8  8284  frrlem14  8290  wfrlem16OLD  8330  smores  8358  smores2  8360  tfrlem13  8396  imafiALT  9351  hartogslem1  9543  wemapso  9552  dmttrcl  9722  r0weon  10013  infxpenlem  10014  brdom3  10529  brdom5  10530  brdom4  10531  fpwwe2lem12  10643  fpwwe2  10644  canth4  10648  canthwelem  10651  pwfseqlem4  10663  nqerf  10931  dmrecnq  10969  uzrdgfni  13930  hashdmpropge2  14451  dmtrclfv  14972  rlimpm  15451  isstruct2  17089  strleun  17097  imasaddfnlem  17481  imasvscafn  17490  isohom  17730  catcoppccl  18077  catcoppcclOLD  18078  tsrss  18552  ledm  18553  dirdm  18563  f1omvdmvd  19359  mvdco  19361  f1omvdconj  19362  pmtrfb  19381  pmtrfconj  19382  symggen  19386  symggen2  19387  pmtrdifellem1  19392  pmtrdifellem2  19393  psgnunilem1  19409  gsum2d  19888  lspextmo  20900  dsmmfi  21604  lindfres  21689  mdetdiaglem  22421  tsmsxp  23980  ustssco  24040  setsmstopn  24307  metustexhalf  24386  tngtopn  24488  equivcau  25149  metsscmetcld  25164  dvbssntr  25750  pserdv  26282  subgreldmiedg  28975  hlimcaui  30924  nfpconfp  32291  symgcom2  32683  pmtrcnel  32688  pmtrcnel2  32689  pmtrcnelor  32690  cycpmrn  32740  metideq  33339  esum2d  33557  subgrwlk  34589  fundmpss  35210  fixssdm  35350  filnetlem3  35732  filnetlem4  35733  ssbnd  37123  bnd2lem  37126  ismrcd1  41902  istopclsd  41904  mptrcllem  42830  cnvrcl0  42842  dmtrcl  42844  dfrcl2  42891  relexpss1d  42922  rfovcnvf1od  43221  fourierdlem80  45364  issmflem  45905