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

Theorem dmeq 5356
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 5355 . . 3 (𝐴𝐵 → dom 𝐴 ⊆ dom 𝐵)
2 dmss 5355 . . 3 (𝐵𝐴 → dom 𝐵 ⊆ dom 𝐴)
31, 2anim12i 589 . 2 ((𝐴𝐵𝐵𝐴) → (dom 𝐴 ⊆ dom 𝐵 ∧ dom 𝐵 ⊆ dom 𝐴))
4 eqss 3651 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
5 eqss 3651 . 2 (dom 𝐴 = dom 𝐵 ↔ (dom 𝐴 ⊆ dom 𝐵 ∧ dom 𝐵 ⊆ dom 𝐴))
63, 4, 53imtr4i 281 1 (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1523  wss 3607  dom cdm 5143
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-dm 5153
This theorem is referenced by:  dmeqi  5357  dmeqd  5358  xpid11  5379  resresdm  5664  fneq1  6017  eqfnfv2  6352  funopdmsn  6455  nvof1o  6576  offval  6946  ofrfval  6947  offval3  7204  suppval  7342  smoeq  7492  tz7.44lem1  7546  tz7.44-2  7548  tz7.44-3  7549  ereq1  7794  fundmeng  8072  fseqenlem2  8886  dfac3  8982  dfac9  8996  dfac12lem1  9003  dfac12r  9006  ackbij2lem2  9100  ackbij2lem3  9101  r1om  9104  cfsmolem  9130  cfsmo  9131  dcomex  9307  axdc2lem  9308  axdc3lem2  9311  axdc3lem4  9313  ac7g  9334  ttukey2g  9376  fundmge2nop0  13312  s4dom  13710  relexp0g  13806  relexpsucnnr  13809  dfrtrcl2  13846  ello1  14290  elo1  14301  bpolylem  14823  bpolyval  14824  isoval  16472  istsr  17264  islindf  20199  decpmatval0  20617  pmatcollpw3lem  20636  ordtval  21041  dfac14  21469  fmval  21794  fmf  21796  blfvalps  22235  tmsval  22333  cfilfval  23108  caufval  23119  isibl  23577  elcpn  23742  iscgrg  25452  uhgr0e  26011  incistruhgr  26019  ausgrusgri  26108  egrsubgr  26214  vtxdgfval  26419  vtxdg0e  26426  1egrvtxdg1  26461  eupth0  27192  ex-dm  27426  f1ocnt  29687  locfinreflem  30035  pstmval  30066  cntnevol  30419  omsval  30483  sitgval  30522  elprob  30599  cndprobval  30623  rrvmbfm  30632  bnj1385  31029  bnj1400  31032  bnj1014  31156  bnj1015  31157  bnj1326  31220  bnj1321  31221  bnj1491  31251  mrsubfval  31531  rdgprc0  31823  dfrdg2  31825  frrlem5e  31913  bdayval  31926  bdayfo  31953  noprefixmo  31973  nosupdm  31975  nosupfv  31977  nosupres  31978  nosupbnd1lem1  31979  nosupbnd1lem3  31981  nosupbnd1lem5  31983  nosupbnd2  31987  noetalem3  31990  brdomaing  32167  fwddifval  32394  fwddifnval  32395  filnetlem4  32501  cureq  33515  ismtyval  33729  isass  33775  isexid  33776  ismgmOLD  33779  elrefrels2  34407  elrefrels3  34408  refreleq  34410  elcnvrefrels2  34420  elcnvrefrels3  34421  elrefsymrels2  34453  aomclem6  37946  aomclem8  37948  dfac21  37953  rclexi  38239  rtrclex  38241  rtrclexi  38245  cnvrcl0  38249  dfrtrcl5  38253  dfrcl2  38283  gneispace2  38747  ssnnf1octb  39696  sge0val  40901  ismea  40986  caragenval  41028  isome  41029  issmflem  41257  fnxpdmdm  42093  offval0  42624  elbigo  42670
  Copyright terms: Public domain W3C validator