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

Theorem dmeq 5233
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 5232 . . 3 (𝐴𝐵 → dom 𝐴 ⊆ dom 𝐵)
2 dmss 5232 . . 3 (𝐵𝐴 → dom 𝐵 ⊆ dom 𝐴)
31, 2anim12i 587 . 2 ((𝐴𝐵𝐵𝐴) → (dom 𝐴 ⊆ dom 𝐵 ∧ dom 𝐵 ⊆ dom 𝐴))
4 eqss 3582 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
5 eqss 3582 . 2 (dom 𝐴 = dom 𝐵 ↔ (dom 𝐴 ⊆ dom 𝐵 ∧ dom 𝐵 ⊆ dom 𝐴))
63, 4, 53imtr4i 279 1 (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1474  wss 3539  dom cdm 5028
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
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 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-br 4578  df-dm 5038
This theorem is referenced by:  dmeqi  5234  dmeqd  5235  xpid11  5255  fneq1  5879  eqfnfv2  6205  nvof1o  6414  offval  6779  ofrfval  6780  offval3  7030  suppval  7161  smoeq  7311  tz7.44lem1  7365  tz7.44-2  7367  tz7.44-3  7368  ereq1  7613  fundmeng  7894  fseqenlem2  8708  dfac3  8804  dfac9  8818  dfac12lem1  8825  dfac12r  8828  ackbij2lem2  8922  ackbij2lem3  8923  r1om  8926  cfsmolem  8952  cfsmo  8953  dcomex  9129  axdc2lem  9130  axdc3lem2  9133  axdc3lem4  9135  ac7g  9156  ttukey2g  9198  s4dom  13460  relexp0g  13556  relexpsucnnr  13559  dfrtrcl2  13596  ello1  14040  elo1  14051  bpolylem  14564  bpolyval  14565  isoval  16194  istsr  16986  islindf  19912  decpmatval0  20330  pmatcollpw3lem  20349  ordtval  20745  dfac14  21173  fmval  21499  fmf  21501  blfvalps  21939  tmsval  22037  cfilfval  22788  caufval  22799  isibl  23255  elcpn  23420  iscgrg  25125  isuhgra  25593  uhgrac  25600  uhgraeq12d  25602  isuslgra  25638  isusgra  25639  usgraeq12d  25657  wlks  25813  wlkcompim  25820  wlkelwrd  25824  ex-dm  26454  f1ocnt  28752  locfinreflem  29041  pstmval  29072  cntnevol  29424  omsval  29488  sitgval  29527  elprob  29604  cndprobval  29628  rrvmbfm  29637  bnj1385  29963  bnj1400  29966  bnj1014  30090  bnj1015  30091  bnj1326  30154  bnj1321  30155  bnj1491  30185  mrsubfval  30465  rdgprc0  30749  dfrdg2  30751  frrlem5e  30838  bdayval  30851  bdayfo  30880  nofulllem5  30911  brdomaing  31018  fwddifval  31245  fwddifnval  31246  filnetlem4  31352  cureq  32351  ismtyval  32565  isass  32611  isexid  32612  ismgmOLD  32615  aomclem6  36443  aomclem8  36445  dfac21  36450  rclexi  36737  rtrclex  36739  rtrclexi  36743  cnvrcl0  36747  dfrtrcl5  36751  dfrcl2  36781  gneispace2  37246  ssnnf1octb  38173  sge0val  39056  ismea  39141  caragenval  39180  isome  39181  issmflem  39410  resresdm  40127  fundmge2nop0  40145  structvtxvallem  40248  uhgr0e  40291  incistruhgr  40300  ausgrusgri  40393  egrsubgr  40496  vtxdgfval  40678  vtxdg0e  40684  1egrvtxdg1  40720  eupth0  41377  fnxpdmdm  41553  offval0  42088  elbigo  42138
  Copyright terms: Public domain W3C validator