Theorem dmeq 5040

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 5039	. . 3 |- ( A C_ B -> dom A C_ dom B )
2		dmss 5039	. . 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 3371	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
5		eqss 3371	. 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 1369   C_ wss 3328   dom cdm 4840

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-rab 2724  df-v 2974  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-sn 3878  df-pr 3880  df-op 3884  df-br 4293  df-dm 4850

This theorem is referenced by:  dmeqi  5041  dmeqd  5042  xpid11  5061  fneq1  5499  eqfnfv2  5798  nvof1o  5987  offval  6327  ofrfval  6328  offval3  6571  suppval  6692  smoeq  6811  tz7.44lem1  6861  tz7.44-2  6863  tz7.44-3  6864  ereq1  7108  fundmeng  7384  fseqenlem2  8195  dfac3  8291  dfac9  8305  dfac12lem1  8312  dfac12r  8315  ackbij2lem2  8409  ackbij2lem3  8410  r1om  8413  cfsmolem  8439  cfsmo  8440  dcomex  8616  axdc2lem  8617  axdc3lem2  8620  axdc3lem4  8622  ac7g  8643  ttukey2g  8685  s4dom  12529  ello1  12993  elo1  13004  isoval  14703  istsr  15387  islindf  18241  ordtval  18793  dfac14  19191  fmval  19516  fmf  19518  blfvalps  19958  tmsval  20056  cfilfval  20775  caufval  20786  isibl  21243  elcpn  21408  iscgrg  22965  isuhgra  23237  uhgraeq12d  23241  isuslgra  23271  isusgra  23272  usgraeq12d  23284  wlks  23425  ex-dm  23646  isass  23803  isexid  23804  ismgm  23807  pstmval  26322  cntnevol  26642  omsval  26708  sitgval  26718  elprob  26792  cndprobval  26816  rrvmbfm  26825  relexpdm  27337  dfrtrcl2  27350  rdgprc0  27607  dfrdg2  27609  frrlem5e  27776  bdayval  27789  bdayfo  27816  nofulllem5  27847  brdomaing  27966  bpolylem  28191  bpolyval  28192  filnetlem4  28602  ismtyval  28699  aomclem6  29412  aomclem8  29414  dfac21  29419  wlkelwrd  30280  wlkcompim  30287  bnj1385  31826  bnj1400  31829  bnj1014  31953  bnj1015  31954  bnj1326  32017  bnj1321  32018  bnj1491  32048