Theorem dmeq 5897

Description: Equality theorem for domain. (Contributed by NM, 11-Aug-1994.)

Assertion

Ref	Expression
dmeq	⊢ (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)

Proof of Theorem dmeq

Step	Hyp	Ref	Expression
1		dmss 5896	. . 3 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)
2		dmss 5896	. . 3 ⊢ (𝐵 ⊆ 𝐴 → dom 𝐵 ⊆ dom 𝐴)
3	1, 2	anim12i 625	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (dom 𝐴 ⊆ dom 𝐵 ∧ dom 𝐵 ⊆ dom 𝐴))
4		eqss 3928	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
5		eqss 3928	. 2 ⊢ (dom 𝐴 = dom 𝐵 ↔ (dom 𝐴 ⊆ dom 𝐵 ∧ dom 𝐵 ⊆ dom 𝐴))
6	3, 4, 5	3imtr4i 295	1 ⊢ (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ⊆ wss 3900  dom cdm 5658

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-br 5109  df-dm 5668

This theorem is used by:  dmeqi  5898  dmeqd  5899  xpid11  5926  resresdm  6253  fneq1  6660  eqfnfv2  7061  funopdmsn  7186  nvof1o  7319  ofrfvalg  7733  offval  7734  offval3  8028  suppval  8216  smoeq  8396  tz7.44lem1  8451  tz7.44-2  8453  tz7.44-3  8454  ereq1  8763  cureq  8927  fundmeng  9098  fseqenlem2  10143  dfac3  10239  dfac9  10254  dfac12lem1  10261  dfac12r  10264  ackbij2lem2  10356  ackbij2lem3  10357  hfom  10360  cfsmolem  10387  cfsmo  10388  dcomex  10564  axdc2lem  10565  axdc3lem2  10568  axdc3lem4  10570  ac7g  10591  ttukey2g  10633  fundmge2nop0  14688  s4dom  15113  relexp0g  15218  relexpsucnnr  15221  dfrtrcl2  15258  ello1  15726  elo1  15737  bpolylem  16258  bpolyval  16259  isoval  17990  istsr  18807  ischn  18831  chnind  18845  islindf  22173  decpmatval0  23137  pmatcollpw3lem  23156  ordtval  23562  dfac14  23992  fmval  24317  fmf  24319  blfvalps  24757  tmsval  24855  cfilfval  25640  caufval  25651  isibl  26141  elcpn  26309  bdayval  28062  bdayfo  28091  nosupprefixmo  28114  noinfprefixmo  28115  nosupcbv  28116  nosupdm  28118  nosupfv  28120  nosupres  28121  nosupbnd1lem1  28122  nosupbnd1lem3  28124  nosupbnd1lem5  28126  nosupbnd2  28130  noinfcbv  28131  noinfdm  28133  noinffv  28135  noinfres  28136  noinfbnd1lem3  28139  noinfbnd1lem5  28141  noetasuplem4  28150  noetainflem4  28154  iscgrg  29032  uhgr0e  29706  incistruhgr  29714  ausgrusgri  29806  egrsubgr  29915  vtxdgfval  30105  vtxdg0e  30112  1egrvtxdg1  30147  eupth0  30872  ex-dm  31097  eldmne0  33319  of0r  33370  f1ocnt  33488  tocycfv  33769  tocycf  33777  tocyc01  33778  cycpmco2f1  33784  cycpmco2rn  33785  cycpmco2lem1  33786  cycpmco2lem2  33787  cycpmco2lem3  33788  cycpmco2lem4  33789  cycpmco2lem5  33790  cycpmco2lem6  33791  cycpmco2lem7  33792  cycpmco2  33793  cycpm3cl2  33796  cycpmconjv  33802  tocyccntz  33804  cyc3evpm  33810  cycpmgcl  33813  cycpmconjslem2  33815  cyc3conja  33817  fxpval  33825  locfinreflem  34583  pstmval  34638  cntnevol  34972  omsval  35036  sitgval  35075  elprob  35152  cndprobval  35176  rrvmbfm  35185  bnj1385  35573  bnj1400  35576  bnj1014  35702  bnj1015  35703  bnj1326  35767  bnj1321  35768  bnj1491  35798  fineqvac  35925  gdlop5fv  36008  fnlfvk30  36068  fnlfvk3n0  36069  srepdflem2  36127  srepdf  36128  mrsubfval  36481  rdgprc0  36770  dfrdg2  36772  brdomaing  36912  fwddifval  37142  fwddifnval  37143  filnetlem4  37384  ismtyval  39000  isass  39046  isexid  39047  ismgmOLD  39050  elrefrels2  39796  elrefrels3  39797  refreleq  39799  elcnvrefrels2  39812  elcnvrefrels3  39813  elrefsymrels2  39851  eleqvrels2  39874  eleqvrels3  39875  dmqseq  39922  aomclem6  44327  aomclem8  44329  dfac21  44334  tfsconcatun  44600  tfsconcat0b  44609  tfsconcatrev  44611  rclexi  44876  rtrclex  44878  rtrclexi  44882  cnvrcl0  44886  dfrtrcl5  44890  dfrcl2  44935  gneispace2  45393  modelaxreplem1  46232  modelaxreplem2  46233  modelaxrep  46235  ackbij3  46289  ssnnf1octb  46482  sge0val  47649  ismea  47734  caragenval  47776  isome  47777  issmflem  48010  isisubgr  49233  isgrim  49253  fnxpdmdm  49530  elbigo  49994  itcoval  50104  iinfprg  50504  infsubc2  50506  fucofvalne  50778