Theorem dmeq 5203

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

Step	Hyp	Ref	Expression
1		dmss 5202	. . 3 |- ( A C_ B -> dom A C_ dom B )
2		dmss 5202	. . 3 |- ( B C_ A -> dom B C_ dom A )
3	1, 2	anim12i 566	. 2 |- ( ( A C_ B /\ B C_ A ) -> ( dom A C_ dom B /\ dom B C_ dom A ) )
4		eqss 3519	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
5		eqss 3519	. 2 |- ( dom A = dom B <-> ( dom A C_ dom B /\ dom B C_ dom A ) )
6	3, 4, 5	3imtr4i 266	1 |- ( A = B -> dom A = dom B )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1379   C_ wss 3476   dom cdm 4999

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448  df-dm 5009

This theorem is referenced by:  dmeqi  5204  dmeqd  5205  xpid11  5224  fneq1  5669  eqfnfv2  5976  nvof1o  6174  offval  6531  ofrfval  6532  offval3  6778  suppval  6903  smoeq  7021  tz7.44lem1  7071  tz7.44-2  7073  tz7.44-3  7074  ereq1  7318  fundmeng  7590  fseqenlem2  8406  dfac3  8502  dfac9  8516  dfac12lem1  8523  dfac12r  8526  ackbij2lem2  8620  ackbij2lem3  8621  r1om  8624  cfsmolem  8650  cfsmo  8651  dcomex  8827  axdc2lem  8828  axdc3lem2  8831  axdc3lem4  8833  ac7g  8854  ttukey2g  8896  s4dom  12830  ello1  13301  elo1  13312  isoval  15020  istsr  15704  islindf  18642  decpmatval0  19060  pmatcollpw3lem  19079  ordtval  19484  dfac14  19882  fmval  20207  fmf  20209  blfvalps  20649  tmsval  20747  cfilfval  21466  caufval  21477  isibl  21935  elcpn  22100  iscgrg  23660  isuhgra  24002  uhgrac  24009  uhgraeq12d  24011  isuslgra  24047  isusgra  24048  usgraeq12d  24066  wlks  24223  wlkcompim  24230  wlkelwrd  24234  ex-dm  24865  isass  25022  isexid  25023  ismgm  25026  pstmval  27538  cntnevol  27867  omsval  27932  sitgval  27942  elprob  28016  cndprobval  28040  rrvmbfm  28049  relexpdm  28561  dfrtrcl2  28574  rdgprc0  28831  dfrdg2  28833  frrlem5e  29000  bdayval  29013  bdayfo  29040  nofulllem5  29071  brdomaing  29190  bpolylem  29415  bpolyval  29416  filnetlem4  29830  ismtyval  29927  aomclem6  30637  aomclem8  30639  dfac21  30644  dirkercncflem2  31432  fourierdlem60  31495  fourierdlem61  31496  uhg0e  31871  uhgres  31874  isfusgra  31919  fnxpdmdm  31959  bnj1385  32988  bnj1400  32991  bnj1014  33115  bnj1015  33116  bnj1326  33179  bnj1321  33180  bnj1491  33210