Theorem dmeq 5904

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 5903	. . 3 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)
2		dmss 5903	. . 3 ⊢ (𝐵 ⊆ 𝐴 → dom 𝐵 ⊆ dom 𝐴)
3	1, 2	anim12i 614	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (dom 𝐴 ⊆ dom 𝐵 ∧ dom 𝐵 ⊆ dom 𝐴))
4		eqss 3998	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
5		eqss 3998	. 2 ⊢ (dom 𝐴 = dom 𝐵 ↔ (dom 𝐴 ⊆ dom 𝐵 ∧ dom 𝐵 ⊆ dom 𝐴))
6	3, 4, 5	3imtr4i 292	1 ⊢ (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542   ⊆ wss 3949  dom cdm 5677

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-dm 5687

This theorem is referenced by:  dmeqi  5905  dmeqd  5906  xpid11  5932  resresdm  6233  fneq1  6641  eqfnfv2  7034  funopdmsn  7148  nvof1o  7278  ofrfvalg  7678  offval  7679  offval3  7969  suppval  8148  smoeq  8350  tz7.44lem1  8405  tz7.44-2  8407  tz7.44-3  8408  ereq1  8710  fundmeng  9032  fseqenlem2  10020  dfac3  10116  dfac9  10131  dfac12lem1  10138  dfac12r  10141  ackbij2lem2  10235  ackbij2lem3  10236  r1om  10239  cfsmolem  10265  cfsmo  10266  dcomex  10442  axdc2lem  10443  axdc3lem2  10446  axdc3lem4  10448  ac7g  10469  ttukey2g  10511  fundmge2nop0  14453  s4dom  14870  relexp0g  14969  relexpsucnnr  14972  dfrtrcl2  15009  ello1  15459  elo1  15470  bpolylem  15992  bpolyval  15993  isoval  17712  istsr  18536  islindf  21367  decpmatval0  22266  pmatcollpw3lem  22285  ordtval  22693  dfac14  23122  fmval  23447  fmf  23449  blfvalps  23889  tmsval  23989  cfilfval  24781  caufval  24792  isibl  25283  elcpn  25451  bdayval  27151  bdayfo  27180  nosupprefixmo  27203  noinfprefixmo  27204  nosupcbv  27205  nosupdm  27207  nosupfv  27209  nosupres  27210  nosupbnd1lem1  27211  nosupbnd1lem3  27213  nosupbnd1lem5  27215  nosupbnd2  27219  noinfcbv  27220  noinfdm  27222  noinffv  27224  noinfres  27225  noinfbnd1lem3  27228  noinfbnd1lem5  27230  noetasuplem4  27239  noetainflem4  27243  iscgrg  27763  uhgr0e  28331  incistruhgr  28339  ausgrusgri  28428  egrsubgr  28534  vtxdgfval  28724  vtxdg0e  28731  1egrvtxdg1  28766  eupth0  29467  ex-dm  29692  eldmne0  31852  f1ocnt  32013  tocycfv  32268  tocycf  32276  tocyc01  32277  cycpmco2f1  32283  cycpmco2rn  32284  cycpmco2lem1  32285  cycpmco2lem2  32286  cycpmco2lem3  32287  cycpmco2lem4  32288  cycpmco2lem5  32289  cycpmco2lem6  32290  cycpmco2lem7  32291  cycpmco2  32292  cycpm3cl2  32295  cycpmconjv  32301  tocyccntz  32303  cyc3evpm  32309  cycpmgcl  32312  cycpmconjslem2  32314  cyc3conja  32316  locfinreflem  32820  pstmval  32875  cntnevol  33226  omsval  33292  sitgval  33331  elprob  33408  cndprobval  33432  rrvmbfm  33441  bnj1385  33843  bnj1400  33846  bnj1014  33972  bnj1015  33973  bnj1326  34037  bnj1321  34038  bnj1491  34068  fineqvac  34097  mrsubfval  34499  rdgprc0  34765  dfrdg2  34767  brdomaing  34907  fwddifval  35134  fwddifnval  35135  filnetlem4  35266  cureq  36464  ismtyval  36668  isass  36714  isexid  36715  ismgmOLD  36718  elrefrels2  37388  elrefrels3  37389  refreleq  37391  elcnvrefrels2  37404  elcnvrefrels3  37405  elrefsymrels2  37439  eleqvrels2  37462  eleqvrels3  37463  dmqseq  37510  aomclem6  41801  aomclem8  41803  dfac21  41808  tfsconcatun  42087  tfsconcat0b  42096  tfsconcatrev  42098  rclexi  42366  rtrclex  42368  rtrclexi  42372  cnvrcl0  42376  dfrtrcl5  42380  dfrcl2  42425  gneispace2  42883  ssnnf1octb  43893  sge0val  45082  ismea  45167  caragenval  45209  isome  45210  issmflem  45443  isomgreqve  46493  fnxpdmdm  46538  elbigo  47237  itcoval  47347