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

Theorem dmeq 5859
Description: Equality theorem for domain. (Contributed by NM, 11-Aug-1994.)
Assertion
Ref Expression
dmeq (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)

Proof of Theorem dmeq
StepHypRef Expression
1 dmss 5858 . . 3 (𝐴𝐵 → dom 𝐴 ⊆ dom 𝐵)
2 dmss 5858 . . 3 (𝐵𝐴 → dom 𝐵 ⊆ dom 𝐴)
31, 2anim12i 613 . 2 ((𝐴𝐵𝐵𝐴) → (dom 𝐴 ⊆ dom 𝐵 ∧ dom 𝐵 ⊆ dom 𝐴))
4 eqss 3959 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
5 eqss 3959 . 2 (dom 𝐴 = dom 𝐵 ↔ (dom 𝐴 ⊆ dom 𝐵 ∧ dom 𝐵 ⊆ dom 𝐴))
63, 4, 53imtr4i 291 1 (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1541  wss 3910  dom cdm 5633
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3408  df-v 3447  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-br 5106  df-dm 5643
This theorem is referenced by:  dmeqi  5860  dmeqd  5861  xpid11  5887  resresdm  6185  fneq1  6593  eqfnfv2  6983  funopdmsn  7096  nvof1o  7226  ofrfvalg  7625  offval  7626  offval3  7915  suppval  8094  smoeq  8296  tz7.44lem1  8351  tz7.44-2  8353  tz7.44-3  8354  ereq1  8655  fundmeng  8976  fseqenlem2  9961  dfac3  10057  dfac9  10072  dfac12lem1  10079  dfac12r  10082  ackbij2lem2  10176  ackbij2lem3  10177  r1om  10180  cfsmolem  10206  cfsmo  10207  dcomex  10383  axdc2lem  10384  axdc3lem2  10387  axdc3lem4  10389  ac7g  10410  ttukey2g  10452  fundmge2nop0  14391  s4dom  14808  relexp0g  14907  relexpsucnnr  14910  dfrtrcl2  14947  ello1  15397  elo1  15408  bpolylem  15931  bpolyval  15932  isoval  17648  istsr  18472  islindf  21218  decpmatval0  22113  pmatcollpw3lem  22132  ordtval  22540  dfac14  22969  fmval  23294  fmf  23296  blfvalps  23736  tmsval  23836  cfilfval  24628  caufval  24639  isibl  25130  elcpn  25298  bdayval  26996  bdayfo  27025  nosupprefixmo  27048  noinfprefixmo  27049  nosupcbv  27050  nosupdm  27052  nosupfv  27054  nosupres  27055  nosupbnd1lem1  27056  nosupbnd1lem3  27058  nosupbnd1lem5  27060  nosupbnd2  27064  noinfcbv  27065  noinfdm  27067  noinffv  27069  noinfres  27070  noinfbnd1lem3  27073  noinfbnd1lem5  27075  noetasuplem4  27084  noetainflem4  27088  iscgrg  27454  uhgr0e  28022  incistruhgr  28030  ausgrusgri  28119  egrsubgr  28225  vtxdgfval  28415  vtxdg0e  28422  1egrvtxdg1  28457  eupth0  29158  ex-dm  29383  eldmne0  31542  f1ocnt  31705  tocycfv  31958  tocycf  31966  tocyc01  31967  cycpmco2f1  31973  cycpmco2rn  31974  cycpmco2lem1  31975  cycpmco2lem2  31976  cycpmco2lem3  31977  cycpmco2lem4  31978  cycpmco2lem5  31979  cycpmco2lem6  31980  cycpmco2lem7  31981  cycpmco2  31982  cycpm3cl2  31985  cycpmconjv  31991  tocyccntz  31993  cyc3evpm  31999  cycpmgcl  32002  cycpmconjslem2  32004  cyc3conja  32006  locfinreflem  32421  pstmval  32476  cntnevol  32827  omsval  32893  sitgval  32932  elprob  33009  cndprobval  33033  rrvmbfm  33042  bnj1385  33444  bnj1400  33447  bnj1014  33573  bnj1015  33574  bnj1326  33638  bnj1321  33639  bnj1491  33669  fineqvac  33698  mrsubfval  34102  rdgprc0  34368  dfrdg2  34370  brdomaing  34520  fwddifval  34747  fwddifnval  34748  filnetlem4  34853  cureq  36054  ismtyval  36259  isass  36305  isexid  36306  ismgmOLD  36309  elrefrels2  36980  elrefrels3  36981  refreleq  36983  elcnvrefrels2  36996  elcnvrefrels3  36997  elrefsymrels2  37031  eleqvrels2  37054  eleqvrels3  37055  dmqseq  37102  aomclem6  41372  aomclem8  41374  dfac21  41379  rclexi  41877  rtrclex  41879  rtrclexi  41883  cnvrcl0  41887  dfrtrcl5  41891  dfrcl2  41936  gneispace2  42394  ssnnf1octb  43404  sge0val  44597  ismea  44682  caragenval  44724  isome  44725  issmflem  44958  isomgreqve  46007  fnxpdmdm  46052  elbigo  46627  itcoval  46737
  Copyright terms: Public domain W3C validator