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

Theorem dmeq 5070
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 5069 . . 3  |-  ( A 
C_  B  ->  dom  A 
C_  dom  B )
2 dmss 5069 . . 3  |-  ( B 
C_  A  ->  dom  B 
C_  dom  A )
31, 2anim12i 550 . 2  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( dom  A  C_  dom  B  /\  dom  B  C_  dom  A ) )
4 eqss 3363 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
5 eqss 3363 . 2  |-  ( dom 
A  =  dom  B  <->  ( dom  A  C_  dom  B  /\  dom  B  C_  dom  A ) )
63, 4, 53imtr4i 258 1  |-  ( A  =  B  ->  dom  A  =  dom  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1652    C_ wss 3320   dom cdm 4878
This theorem is referenced by:  dmeqi  5071  dmeqd  5072  xpid11  5091  fneq1  5534  eqfnfv2  5828  offval  6312  ofrfval  6313  offval3  6318  smoeq  6612  tz7.44lem1  6663  tz7.44-2  6665  tz7.44-3  6666  ereq1  6912  fundmeng  7181  fseqenlem2  7906  dfac3  8002  dfac9  8016  dfac12lem1  8023  dfac12r  8026  ackbij2lem2  8120  ackbij2lem3  8121  r1om  8124  cfsmolem  8150  cfsmo  8151  dcomex  8327  axdc2lem  8328  axdc3lem2  8331  axdc3lem4  8333  ac7g  8354  ttukey2g  8396  s4dom  11866  ello1  12309  elo1  12320  isoval  13990  istsr  14649  isla  14665  ordtval  17253  dfac14  17650  fmval  17975  fmf  17977  blfvalps  18413  tmsval  18511  cfilfval  19217  caufval  19228  isibl  19657  elcpn  19820  isuhgra  21338  uhgraeq12d  21342  isuslgra  21372  isusgra  21373  usgraeq12d  21385  wlks  21526  ex-dm  21747  isass  21904  isexid  21905  ismgm  21908  nvof1o  24040  pstmval  24290  cntnevol  24582  sitgval  24647  elprob  24667  cndprobval  24691  rrvmbfm  24700  relexpdm  25135  dfrtrcl2  25148  rdgprc0  25421  dfrdg2  25423  frrlem5e  25590  bdayval  25603  bdayfo  25630  nofulllem5  25661  brdomaing  25780  bpolylem  26094  bpolyval  26095  filnetlem4  26410  ismtyval  26509  aomclem6  27134  aomclem8  27136  dfac21  27141  islindf  27259  wlkelwrd  28295  wlkcompim  28302  bnj1385  29204  bnj1400  29207  bnj1014  29331  bnj1015  29332  bnj1326  29395  bnj1321  29396  bnj1491  29426
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rab 2714  df-v 2958  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-op 3823  df-br 4213  df-dm 4888
  Copyright terms: Public domain W3C validator