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

Theorem dmeq 4895
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 4894 . . 3  |-  ( A 
C_  B  ->  dom  A 
C_  dom  B )
2 dmss 4894 . . 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 3207 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
5 eqss 3207 . 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 1632    C_ wss 3165   dom cdm 4705
This theorem is referenced by:  dmeqi  4896  dmeqd  4897  xpid11  4916  fneq1  5349  eqfnfv2  5639  offval  6101  ofrfval  6102  offval3  6107  smoeq  6383  tz7.44lem1  6434  tz7.44-2  6436  tz7.44-3  6437  ereq1  6683  fundmeng  6951  fseqenlem2  7668  dfac3  7764  dfac9  7778  dfac12lem1  7785  dfac12r  7788  ackbij2lem2  7882  ackbij2lem3  7883  r1om  7886  cfsmolem  7912  cfsmo  7913  dcomex  8089  axdc2lem  8090  axdc3lem2  8093  axdc3lem4  8095  ac7g  8117  ttukey2g  8159  ello1  12005  elo1  12016  isoval  13683  istsr  14342  isla  14358  ordtval  16935  dfac14  17328  fmval  17654  fmf  17656  blfval  17963  tmsval  18043  cfilfval  18706  caufval  18717  isibl  19136  elcpn  19299  ex-dm  20842  isass  20999  isexid  21000  ismgm  21003  nvof1o  23052  cntnevol  23191  elprob  23627  cndprobval  23651  rrvmbfm  23660  relexpdm  24047  dfrtrcl2  24060  rdgprc0  24221  dfrdg2  24223  frrlem5e  24360  bdayval  24373  bdayfo  24400  nofulllem5  24431  brdomaing  24545  bpolylem  24855  bpolyval  24856  iscst1  25277  islatalg  25286  cur1val  25301  valcurfn1  25307  gepsup  25353  seinf  25354  iscom  25436  rngmgmbs3  25520  rngodmeqrn  25522  svs2  25590  istopx  25650  ismgra  25813  isalg  25824  algi  25830  isded  25839  dedi  25840  iscatOLD  25857  cati  25858  pfsubkl  26150  pgapspf  26155  pgapspf2  26156  filnetlem4  26433  ismtyval  26627  aomclem6  27259  aomclem8  27262  dfac21  27267  islindf  27385  stoweidlem27  27879  s4dom  28224  isuslgra  28234  isusgra  28235  usgraeq12d  28245  wlks  28328  bnj1385  29181  bnj1400  29184  bnj1014  29308  bnj1015  29309  bnj1326  29372  bnj1321  29373  bnj1491  29403
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-br 4040  df-dm 4715
  Copyright terms: Public domain W3C validator