Theorem dmeq 5036

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 5035	. . 3 |- ( A C_ B -> dom A C_ dom B )
2		dmss 5035	. . 3 |- ( B C_ A -> dom B C_ dom A )
3	1, 2	anim12i 563	. 2 |- ( ( A C_ B /\ B C_ A ) -> ( dom A C_ dom B /\ dom B C_ dom A ) )
4		eqss 3368	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
5		eqss 3368	. 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 1364   C_ wss 3325   dom cdm 4836

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-rab 2722  df-v 2972  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-sn 3875  df-pr 3877  df-op 3881  df-br 4290  df-dm 4846

This theorem is referenced by:  dmeqi  5037  dmeqd  5038  xpid11  5057  fneq1  5496  eqfnfv2  5795  nvof1o  5984  offval  6326  ofrfval  6327  offval3  6570  suppval  6691  smoeq  6807  tz7.44lem1  6857  tz7.44-2  6859  tz7.44-3  6860  ereq1  7104  fundmeng  7380  fseqenlem2  8191  dfac3  8287  dfac9  8301  dfac12lem1  8308  dfac12r  8311  ackbij2lem2  8405  ackbij2lem3  8406  r1om  8409  cfsmolem  8435  cfsmo  8436  dcomex  8612  axdc2lem  8613  axdc3lem2  8616  axdc3lem4  8618  ac7g  8639  ttukey2g  8681  s4dom  12525  ello1  12989  elo1  13000  isoval  14699  istsr  15383  islindf  18200  ordtval  18752  dfac14  19150  fmval  19475  fmf  19477  blfvalps  19917  tmsval  20015  cfilfval  20734  caufval  20745  isibl  21202  elcpn  21367  iscgrg  22924  isuhgra  23172  uhgraeq12d  23176  isuslgra  23206  isusgra  23207  usgraeq12d  23219  wlks  23360  ex-dm  23581  isass  23738  isexid  23739  ismgm  23742  pstmval  26258  cntnevol  26578  sitgval  26648  elprob  26722  cndprobval  26746  rrvmbfm  26755  relexpdm  27266  dfrtrcl2  27279  rdgprc0  27536  dfrdg2  27538  frrlem5e  27705  bdayval  27718  bdayfo  27745  nofulllem5  27776  brdomaing  27895  bpolylem  28120  bpolyval  28121  filnetlem4  28527  ismtyval  28624  aomclem6  29337  aomclem8  29339  dfac21  29344  wlkelwrd  30205  wlkcompim  30212  bnj1385  31660  bnj1400  31663  bnj1014  31787  bnj1015  31788  bnj1326  31851  bnj1321  31852  bnj1491  31882