Theorem dmeq 5035

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 5034	. . 3 |- ( A C_ B -> dom A C_ dom B )
2		dmss 5034	. . 3 |- ( B C_ A -> dom B C_ dom A )
3	1, 2	anim12i 570	. 2 |- ( ( A C_ B /\ B C_ A ) -> ( dom A C_ dom B /\ dom B C_ dom A ) )
4		eqss 3447	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
5		eqss 3447	. 2 |- ( dom A = dom B <-> ( dom A C_ dom B /\ dom B C_ dom A ) )
6	3, 4, 5	3imtr4i 270	1 |- ( A = B -> dom A = dom B )

Syntax hints:   -> wi 4   /\ wa 371   = wceq 1444   C_ wss 3404   dom cdm 4834

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-rab 2746  df-v 3047  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-sn 3969  df-pr 3971  df-op 3975  df-br 4403  df-dm 4844

This theorem is referenced by:  dmeqi  5036  dmeqd  5037  xpid11  5056  fneq1  5664  eqfnfv2  5977  nvof1o  6179  offval  6538  ofrfval  6539  offval3  6787  suppval  6916  smoeq  7069  tz7.44lem1  7123  tz7.44-2  7125  tz7.44-3  7126  ereq1  7370  fundmeng  7644  fseqenlem2  8456  dfac3  8552  dfac9  8566  dfac12lem1  8573  dfac12r  8576  ackbij2lem2  8670  ackbij2lem3  8671  r1om  8674  cfsmolem  8700  cfsmo  8701  dcomex  8877  axdc2lem  8878  axdc3lem2  8881  axdc3lem4  8883  ac7g  8904  ttukey2g  8946  s4dom  13004  relexp0g  13085  relexpsucnnr  13088  dfrtrcl2  13125  ello1  13579  elo1  13590  bpolylem  14101  bpolyval  14102  isoval  15670  istsr  16463  islindf  19370  decpmatval0  19788  pmatcollpw3lem  19807  ordtval  20205  dfac14  20633  fmval  20958  fmf  20960  blfvalps  21398  tmsval  21496  cfilfval  22234  caufval  22245  isibl  22723  elcpn  22888  iscgrg  24557  isuhgra  25025  uhgrac  25032  uhgraeq12d  25034  isuslgra  25070  isusgra  25071  usgraeq12d  25089  wlks  25247  wlkcompim  25254  wlkelwrd  25258  ex-dm  25889  isass  26044  isexid  26045  ismgmOLD  26048  f1ocnt  28376  locfinreflem  28667  pstmval  28698  cntnevol  29050  omsval  29117  omsvalOLD  29121  sitgval  29165  elprob  29242  cndprobval  29266  rrvmbfm  29275  bnj1385  29644  bnj1400  29647  bnj1014  29771  bnj1015  29772  bnj1326  29835  bnj1321  29836  bnj1491  29866  mrsubfval  30146  rdgprc0  30440  dfrdg2  30442  frrlem5e  30522  bdayval  30535  bdayfo  30564  nofulllem5  30595  brdomaing  30702  fwddifval  30929  fwddifnval  30930  filnetlem4  31037  ismtyval  32132  aomclem6  35917  aomclem8  35919  dfac21  35924  rclexi  36222  rtrclex  36224  rtrclexi  36228  cnvrcl0  36232  dfrtrcl5  36236  dfrcl2  36266  ssnnf1octb  37470  sge0val  38208  ismea  38289  caragenval  38314  isome  38315  resresdm  39010  fundmge2nop  39026  structvtxvallem  39122  uhgr0e  39164  incistruhgr  39171  ausgrusgri  39255  egrsubgr  39349  vtxdgfval  39528  vtxdg0e  39534  uhg0e  39741  uhgres  39744  isfusgra  39789  fnxpdmdm  39821  offval0  40356  elbigo  40415