Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  dmss Structured version   Visualization version   GIF version

Theorem dmss 5758
 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.
StepHypRef Expression
1 ssel 3946 . . . 4 (𝐴𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
21eximdv 1919 . . 3 (𝐴𝐵 → (∃𝑦𝑥, 𝑦⟩ ∈ 𝐴 → ∃𝑦𝑥, 𝑦⟩ ∈ 𝐵))
3 vex 3483 . . . 4 𝑥 ∈ V
43eldm2 5757 . . 3 (𝑥 ∈ dom 𝐴 ↔ ∃𝑦𝑥, 𝑦⟩ ∈ 𝐴)
53eldm2 5757 . . 3 (𝑥 ∈ dom 𝐵 ↔ ∃𝑦𝑥, 𝑦⟩ ∈ 𝐵)
62, 4, 53imtr4g 299 . 2 (𝐴𝐵 → (𝑥 ∈ dom 𝐴𝑥 ∈ dom 𝐵))
76ssrdv 3959 1 (𝐴𝐵 → dom 𝐴 ⊆ dom 𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∃wex 1781   ∈ wcel 2115   ⊆ wss 3919  ⟨cop 4556  dom cdm 5542 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 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-v 3482  df-un 3924  df-in 3926  df-ss 3936  df-sn 4551  df-pr 4553  df-op 4557  df-br 5053  df-dm 5552 This theorem is referenced by:  dmeq  5759  dmv  5779  rnss  5796  dmiin  5812  ssxpb  6018  sofld  6031  relrelss  6111  funssxp  6525  fndmdif  6803  fneqeql2  6808  dff3  6857  frxp  7816  fnwelem  7821  funsssuppss  7852  tposss  7889  wfrlem16  7966  smores  7985  smores2  7987  tfrlem13  8022  imafi  8814  hartogslem1  9003  wemapso  9012  r0weon  9436  infxpenlem  9437  brdom3  9948  brdom5  9949  brdom4  9950  fpwwe2lem13  10062  fpwwe2  10063  canth4  10067  canthwelem  10070  pwfseqlem4  10082  nqerf  10350  dmrecnq  10388  uzrdgfni  13330  hashdmpropge2  13846  dmtrclfv  14378  rlimpm  14857  isstruct2  16493  strleun  16591  imasaddfnlem  16801  imasvscafn  16810  isohom  17046  catcoppccl  17368  tsrss  17833  ledm  17834  dirdm  17844  f1omvdmvd  18571  mvdco  18573  f1omvdconj  18574  pmtrfb  18593  pmtrfconj  18594  symggen  18598  symggen2  18599  pmtrdifellem1  18604  pmtrdifellem2  18605  psgnunilem1  18621  gsum2d  19092  lspextmo  19828  dsmmfi  20434  lindfres  20519  mdetdiaglem  21210  tsmsxp  22766  ustssco  22826  setsmstopn  23091  metustexhalf  23169  tngtopn  23262  equivcau  23910  metsscmetcld  23925  dvbssntr  24509  pserdv  25030  subgreldmiedg  27079  hlimcaui  29025  nfpconfp  30391  symgcom2  30763  pmtrcnel  30768  pmtrcnel2  30769  pmtrcnelor  30770  cycpmrn  30820  metideq  31196  esum2d  31412  subgrwlk  32439  fundmpss  33069  frrlem8  33190  frrlem14  33196  fixssdm  33427  filnetlem3  33788  filnetlem4  33789  ssbnd  35174  bnd2lem  35177  ismrcd1  39559  istopclsd  39561  mptrcllem  40233  cnvrcl0  40245  dmtrcl  40247  dfrcl2  40295  relexpss1d  40326  rp-imass  40393  rfovcnvf1od  40626  fourierdlem80  42758  issmflem  43291
 Copyright terms: Public domain W3C validator