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

Theorem dmss 5312
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 3589 . . . 4 (𝐴𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
21eximdv 1844 . . 3 (𝐴𝐵 → (∃𝑦𝑥, 𝑦⟩ ∈ 𝐴 → ∃𝑦𝑥, 𝑦⟩ ∈ 𝐵))
3 vex 3198 . . . 4 𝑥 ∈ V
43eldm2 5311 . . 3 (𝑥 ∈ dom 𝐴 ↔ ∃𝑦𝑥, 𝑦⟩ ∈ 𝐴)
53eldm2 5311 . . 3 (𝑥 ∈ dom 𝐵 ↔ ∃𝑦𝑥, 𝑦⟩ ∈ 𝐵)
62, 4, 53imtr4g 285 . 2 (𝐴𝐵 → (𝑥 ∈ dom 𝐴𝑥 ∈ dom 𝐵))
76ssrdv 3601 1 (𝐴𝐵 → dom 𝐴 ⊆ dom 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1702  wcel 1988  wss 3567  cop 4174  dom cdm 5104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-br 4645  df-dm 5114
This theorem is referenced by:  dmeq  5313  dmv  5330  rnss  5343  dmiin  5358  ssxpb  5556  sofld  5569  relrelss  5647  funssxp  6048  fndmdif  6307  fneqeql2  6312  dff3  6358  frxp  7272  fnwelem  7277  funsssuppss  7306  tposss  7338  wfrlem16  7415  smores  7434  smores2  7436  tfrlem13  7471  imafi  8244  hartogslem1  8432  wemapso  8441  r0weon  8820  infxpenlem  8821  brdom3  9335  brdom5  9336  brdom4  9337  fpwwe2lem13  9449  fpwwe2  9450  canth4  9454  canthwelem  9457  pwfseqlem4  9469  nqerf  9737  dmrecnq  9775  uzrdgfni  12740  hashdmpropge2  13248  dmtrclfv  13740  rlimpm  14212  isstruct2  15848  strlemor1OLD  15950  strleun  15953  imasaddfnlem  16169  imasvscafn  16178  isohom  16417  catcoppccl  16739  tsrss  17204  ledm  17205  dirdm  17215  f1omvdmvd  17844  mvdco  17846  f1omvdconj  17847  pmtrfb  17866  pmtrfconj  17867  symggen  17871  symggen2  17872  pmtrdifellem1  17877  pmtrdifellem2  17878  psgnunilem1  17894  gsum2d  18352  lspextmo  19037  dsmmfi  20063  lindfres  20143  mdetdiaglem  20385  tsmsxp  21939  ustssco  21999  setsmstopn  22264  metustexhalf  22342  tngtopn  22435  equivcau  23079  cmetss  23094  dvbssntr  23645  pserdv  24164  structgrssvtxlemOLD  25896  subgreldmiedg  26156  hlimcaui  28063  metideq  29910  esum2d  30129  fundmpss  31640  fixssdm  31988  filnetlem3  32350  filnetlem4  32351  ssbnd  33558  bnd2lem  33561  ismrcd1  37080  istopclsd  37082  mptrcllem  37739  cnvrcl0  37751  dmtrcl  37753  dfrcl2  37785  relexpss1d  37816  rp-imass  37885  rfovcnvf1od  38118  fourierdlem80  40166  issmflem  40699
  Copyright terms: Public domain W3C validator