Theorem dmeq 5324

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 5323	. . 3 |- ( A C_ B -> dom A C_ dom B )
2		dmss 5323	. . 3 |- ( B C_ A -> dom B C_ dom A )
3	1, 2	anim12i 590	. 2 |- ( ( A C_ B /\ B C_ A ) -> ( dom A C_ dom B /\ dom B C_ dom A ) )
4		eqss 3618	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
5		eqss 3618	. 2 |- ( dom A = dom B <-> ( dom A C_ dom B /\ dom B C_ dom A ) )
6	3, 4, 5	3imtr4i 281	1 |- ( A = B -> dom A = dom B )

Syntax hints:   -> wi 4   /\ wa 384   = wceq 1483   C_ wss 3574   dom cdm 5114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-dm 5124

This theorem is referenced by:  dmeqi  5325  dmeqd  5326  xpid11  5347  resresdm  5626  fneq1  5979  eqfnfv2  6312  funopdmsn  6415  nvof1o  6536  offval  6904  ofrfval  6905  offval3  7162  suppval  7297  smoeq  7447  tz7.44lem1  7501  tz7.44-2  7503  tz7.44-3  7504  ereq1  7749  fundmeng  8031  fseqenlem2  8848  dfac3  8944  dfac9  8958  dfac12lem1  8965  dfac12r  8968  ackbij2lem2  9062  ackbij2lem3  9063  r1om  9066  cfsmolem  9092  cfsmo  9093  dcomex  9269  axdc2lem  9270  axdc3lem2  9273  axdc3lem4  9275  ac7g  9296  ttukey2g  9338  fundmge2nop0  13274  s4dom  13664  relexp0g  13762  relexpsucnnr  13765  dfrtrcl2  13802  ello1  14246  elo1  14257  bpolylem  14779  bpolyval  14780  isoval  16425  istsr  17217  islindf  20151  decpmatval0  20569  pmatcollpw3lem  20588  ordtval  20993  dfac14  21421  fmval  21747  fmf  21749  blfvalps  22188  tmsval  22286  cfilfval  23062  caufval  23073  isibl  23532  elcpn  23697  iscgrg  25407  uhgr0e  25966  incistruhgr  25974  ausgrusgri  26063  egrsubgr  26169  vtxdgfval  26363  vtxdg0e  26370  1egrvtxdg1  26405  eupth0  27074  ex-dm  27296  f1ocnt  29559  locfinreflem  29907  pstmval  29938  cntnevol  30291  omsval  30355  sitgval  30394  elprob  30471  cndprobval  30495  rrvmbfm  30504  bnj1385  30903  bnj1400  30906  bnj1014  31030  bnj1015  31031  bnj1326  31094  bnj1321  31095  bnj1491  31125  mrsubfval  31405  rdgprc0  31699  dfrdg2  31701  frrlem5e  31788  bdayval  31801  bdayfo  31828  noprefixmo  31848  nosupdm  31850  nosupfv  31852  nosupres  31853  nosupbnd1lem1  31854  nosupbnd1lem3  31856  nosupbnd1lem5  31858  nosupbnd2  31862  noetalem3  31865  brdomaing  32042  fwddifval  32269  fwddifnval  32270  filnetlem4  32376  cureq  33385  ismtyval  33599  isass  33645  isexid  33646  ismgmOLD  33649  aomclem6  37629  aomclem8  37631  dfac21  37636  rclexi  37922  rtrclex  37924  rtrclexi  37928  cnvrcl0  37932  dfrtrcl5  37936  dfrcl2  37966  gneispace2  38430  ssnnf1octb  39382  sge0val  40583  ismea  40668  caragenval  40707  isome  40708  issmflem  40936  fnxpdmdm  41768  offval0  42299  elbigo  42345