Theorem dmeq 5029

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 5028	. . 3 |- ( A C_ B -> dom A C_ dom B )
2		dmss 5028	. . 3 |- ( B C_ A -> dom B C_ dom A )
3	1, 2	anim12i 550	. 2 |- ( ( A C_ B /\ B C_ A ) -> ( dom A C_ dom B /\ dom B C_ dom A ) )
4		eqss 3323	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
5		eqss 3323	. 2 |- ( dom A = dom B <-> ( dom A C_ dom B /\ dom B C_ dom A ) )
6	3, 4, 5	3imtr4i 258	1 |- ( A = B -> dom A = dom B )

Syntax hints:   -> wi 4   /\ wa 359   = wceq 1649   C_ wss 3280   dom cdm 4837

This theorem is referenced by:  dmeqi  5030  dmeqd  5031  xpid11  5050  fneq1  5493  eqfnfv2  5787  offval  6271  ofrfval  6272  offval3  6277  smoeq  6571  tz7.44lem1  6622  tz7.44-2  6624  tz7.44-3  6625  ereq1  6871  fundmeng  7140  fseqenlem2  7862  dfac3  7958  dfac9  7972  dfac12lem1  7979  dfac12r  7982  ackbij2lem2  8076  ackbij2lem3  8077  r1om  8080  cfsmolem  8106  cfsmo  8107  dcomex  8283  axdc2lem  8284  axdc3lem2  8287  axdc3lem4  8289  ac7g  8310  ttukey2g  8352  s4dom  11821  ello1  12264  elo1  12275  isoval  13945  istsr  14604  isla  14620  ordtval  17207  dfac14  17603  fmval  17928  fmf  17930  blfvalps  18366  tmsval  18464  cfilfval  19170  caufval  19181  isibl  19610  elcpn  19773  isuhgra  21291  uhgraeq12d  21295  isuslgra  21325  isusgra  21326  usgraeq12d  21338  wlks  21479  ex-dm  21700  isass  21857  isexid  21858  ismgm  21861  nvof1o  23993  pstmval  24243  cntnevol  24535  sitgval  24600  elprob  24620  cndprobval  24644  rrvmbfm  24653  relexpdm  25088  dfrtrcl2  25101  rdgprc0  25364  dfrdg2  25366  frrlem5e  25503  bdayval  25516  bdayfo  25543  nofulllem5  25574  brdomaing  25688  bpolylem  25998  bpolyval  25999  filnetlem4  26300  ismtyval  26399  aomclem6  27024  aomclem8  27027  dfac21  27032  islindf  27150  bnj1385  28910  bnj1400  28913  bnj1014  29037  bnj1015  29038  bnj1326  29101  bnj1321  29102  bnj1491  29132

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173  df-dm 4847