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

Theorem dmss 5227
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 3556 . . . 4 (𝐴𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
21eximdv 1831 . . 3 (𝐴𝐵 → (∃𝑦𝑥, 𝑦⟩ ∈ 𝐴 → ∃𝑦𝑥, 𝑦⟩ ∈ 𝐵))
3 vex 3170 . . . 4 𝑥 ∈ V
43eldm2 5226 . . 3 (𝑥 ∈ dom 𝐴 ↔ ∃𝑦𝑥, 𝑦⟩ ∈ 𝐴)
53eldm2 5226 . . 3 (𝑥 ∈ dom 𝐵 ↔ ∃𝑦𝑥, 𝑦⟩ ∈ 𝐵)
62, 4, 53imtr4g 283 . 2 (𝐴𝐵 → (𝑥 ∈ dom 𝐴𝑥 ∈ dom 𝐵))
76ssrdv 3568 1 (𝐴𝐵 → dom 𝐴 ⊆ dom 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1694  wcel 1975  wss 3534  cop 4125  dom cdm 5023
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2227  ax-ext 2584
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2591  df-cleq 2597  df-clel 2600  df-nfc 2734  df-rab 2899  df-v 3169  df-dif 3537  df-un 3539  df-in 3541  df-ss 3548  df-nul 3869  df-if 4031  df-sn 4120  df-pr 4122  df-op 4126  df-br 4573  df-dm 5033
This theorem is referenced by:  dmeq  5228  dmv  5244  rnss  5257  dmiin  5272  ssxpb  5468  sofld  5481  relrelss  5557  funssxp  5955  fndmdif  6209  fneqeql2  6214  dff3  6260  frxp  7146  fnwelem  7151  funsssuppss  7180  tposss  7212  wfrlem16  7289  smores  7308  smores2  7310  tfrlem13  7345  imafi  8114  hartogslem1  8302  wemapso  8311  r0weon  8690  infxpenlem  8691  brdom3  9203  brdom5  9204  brdom4  9205  fpwwe2lem13  9315  fpwwe2  9316  canth4  9320  canthwelem  9323  pwfseqlem4  9335  nqerf  9603  dmrecnq  9641  uzrdgfni  12569  dmtrclfv  13548  rlimpm  14020  isstruct2  15645  strlemor1  15737  strleun  15740  imasaddfnlem  15952  imasvscafn  15961  isohom  16200  catcoppccl  16522  tsrss  16987  ledm  16988  dirdm  16998  f1omvdmvd  17627  mvdco  17629  f1omvdconj  17630  pmtrfb  17649  pmtrfconj  17650  symggen  17654  symggen2  17655  pmtrdifellem1  17660  pmtrdifellem2  17661  psgnunilem1  17677  gsum2d  18135  lspextmo  18818  dsmmfi  19838  lindfres  19918  mdetdiaglem  20160  tsmsxp  21705  ustssco  21765  setsmstopn  22029  metustexhalf  22107  tngtopn  22197  equivcau  22819  cmetss  22833  dvbssntr  23382  pserdv  23899  uhgrares  25598  umgrares  25614  usgrares  25659  hlimcaui  27278  metideq  29065  esum2d  29283  fundmpss  30711  fixssdm  30984  filnetlem3  31346  filnetlem4  31347  ssbnd  32555  bnd2lem  32558  ismrcd1  36077  istopclsd  36079  mptrcllem  36737  cnvrcl0  36749  dmtrcl  36751  dfrcl2  36783  relexpss1d  36814  rp-imass  36883  rfovcnvf1od  37116  fourierdlem80  38878  issmflem  39412  structgrssvtxlem  40253  subgreldmiedg  40504
  Copyright terms: Public domain W3C validator