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

Theorem dmeq 4879
Description: Equality theorem for domain. (Contributed by NM, 11-Aug-1994.)
Assertion
Ref Expression
dmeq  |-  ( A  =  B  ->  dom  A  =  dom  B )

Proof of Theorem dmeq
StepHypRef Expression
1 dmss 4878 . . 3  |-  ( A 
C_  B  ->  dom  A 
C_  dom  B )
2 dmss 4878 . . 3  |-  ( B 
C_  A  ->  dom  B 
C_  dom  A )
31, 2anim12i 549 . 2  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( dom  A  C_  dom  B  /\  dom  B  C_  dom  A ) )
4 eqss 3194 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
5 eqss 3194 . 2  |-  ( dom 
A  =  dom  B  <->  ( dom  A  C_  dom  B  /\  dom  B  C_  dom  A ) )
63, 4, 53imtr4i 257 1  |-  ( A  =  B  ->  dom  A  =  dom  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1623    C_ wss 3152   dom cdm 4689
This theorem is referenced by:  dmeqi  4880  dmeqd  4881  xpid11  4900  fneq1  5333  eqfnfv2  5623  offval  6085  ofrfval  6086  offval3  6091  smoeq  6367  tz7.44lem1  6418  tz7.44-2  6420  tz7.44-3  6421  ereq1  6667  fundmeng  6935  fseqenlem2  7652  dfac3  7748  dfac9  7762  dfac12lem1  7769  dfac12r  7772  ackbij2lem2  7866  ackbij2lem3  7867  r1om  7870  cfsmolem  7896  cfsmo  7897  dcomex  8073  axdc2lem  8074  axdc3lem2  8077  axdc3lem4  8079  ac7g  8101  ttukey2g  8143  ello1  11989  elo1  12000  isoval  13667  istsr  14326  isla  14342  ordtval  16919  dfac14  17312  fmval  17638  fmf  17640  blfval  17947  tmsval  18027  cfilfval  18690  caufval  18701  isibl  19120  elcpn  19283  ex-dm  20826  isass  20983  isexid  20984  ismgm  20987  nvof1o  23036  cntnevol  23175  elprob  23612  cndprobval  23636  rrvmbfm  23645  relexpdm  24032  dfrtrcl2  24045  rdgprc0  24150  dfrdg2  24152  frrlem5e  24289  bdayval  24302  bdayfo  24329  nofulllem5  24360  brdomaing  24474  bpolylem  24783  bpolyval  24784  iscst1  25174  islatalg  25183  cur1val  25198  valcurfn1  25204  gepsup  25250  seinf  25251  iscom  25333  rngmgmbs3  25417  rngodmeqrn  25419  svs2  25487  istopx  25547  ismgra  25710  isalg  25721  algi  25727  isded  25736  dedi  25737  iscatOLD  25754  cati  25755  pfsubkl  26047  pgapspf  26052  pgapspf2  26053  filnetlem4  26330  ismtyval  26524  aomclem6  27156  aomclem8  27159  dfac21  27164  islindf  27282  stoweidlem27  27776  s4dom  28092  isuslgra  28102  isusgra  28103  usgraeq12d  28111  bnj1385  28865  bnj1400  28868  bnj1014  28992  bnj1015  28993  bnj1326  29056  bnj1321  29057  bnj1491  29087
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024  df-dm 4699
  Copyright terms: Public domain W3C validator