Theorem dmeq 5875

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 5874	. . 3 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)
2		dmss 5874	. . 3 ⊢ (𝐵 ⊆ 𝐴 → dom 𝐵 ⊆ dom 𝐴)
3	1, 2	anim12i 622	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (dom 𝐴 ⊆ dom 𝐵 ∧ dom 𝐵 ⊆ dom 𝐴))
4		eqss 3949	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
5		eqss 3949	. 2 ⊢ (dom 𝐴 = dom 𝐵 ↔ (dom 𝐴 ⊆ dom 𝐵 ∧ dom 𝐵 ⊆ dom 𝐴))
6	3, 4, 5	3imtr4i 294	1 ⊢ (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1559   ⊆ wss 3902  dom cdm 5643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098  df-dm 5653

This theorem is referenced by:  dmeqi  5876  dmeqd  5877  xpid11  5904  resresdm  6215  fneq1  6607  eqfnfv2  7007  funopdmsn  7128  nvof1o  7259  ofrfvalg  7663  offval  7664  offval3  7958  suppval  8136  smoeq  8315  tz7.44lem1  8370  tz7.44-2  8372  tz7.44-3  8373  ereq1  8680  fundmeng  9007  fseqenlem2  9975  dfac3  10071  dfac9  10087  dfac12lem1  10094  dfac12r  10097  ackbij2lem2  10189  ackbij2lem3  10190  r1om  10193  cfsmolem  10221  cfsmo  10222  dcomex  10398  axdc2lem  10399  axdc3lem2  10402  axdc3lem4  10404  ac7g  10425  ttukey2g  10467  fundmge2nop0  14509  s4dom  14926  relexp0g  15029  relexpsucnnr  15032  dfrtrcl2  15069  ello1  15533  elo1  15544  bpolylem  16069  bpolyval  16070  isoval  17789  istsr  18606  ischn  18630  chnind  18644  islindf  21852  decpmatval0  22812  pmatcollpw3lem  22831  ordtval  23237  dfac14  23666  fmval  23991  fmf  23993  blfvalps  24431  tmsval  24529  cfilfval  25314  caufval  25325  isibl  25815  elcpn  25984  bdayval  27700  bdayfo  27729  nosupprefixmo  27752  noinfprefixmo  27753  nosupcbv  27754  nosupdm  27756  nosupfv  27758  nosupres  27759  nosupbnd1lem1  27760  nosupbnd1lem3  27762  nosupbnd1lem5  27764  nosupbnd2  27768  noinfcbv  27769  noinfdm  27771  noinffv  27773  noinfres  27774  noinfbnd1lem3  27777  noinfbnd1lem5  27779  noetasuplem4  27788  noetainflem4  27792  iscgrg  28669  uhgr0e  29229  incistruhgr  29237  ausgrusgri  29326  egrsubgr  29435  vtxdgfval  29625  vtxdg0e  29632  1egrvtxdg1  29667  eupth0  30373  ex-dm  30598  eldmne0  32790  of0r  32842  f1ocnt  32963  tocycfv  33250  tocycf  33258  tocyc01  33259  cycpmco2f1  33265  cycpmco2rn  33266  cycpmco2lem1  33267  cycpmco2lem2  33268  cycpmco2lem3  33269  cycpmco2lem4  33270  cycpmco2lem5  33271  cycpmco2lem6  33272  cycpmco2lem7  33273  cycpmco2  33274  cycpm3cl2  33277  cycpmconjv  33283  tocyccntz  33285  cyc3evpm  33291  cycpmgcl  33294  cycpmconjslem2  33296  cyc3conja  33298  fxpval  33306  locfinreflem  34098  pstmval  34153  cntnevol  34486  omsval  34551  sitgval  34590  elprob  34667  cndprobval  34691  rrvmbfm  34700  bnj1385  35088  bnj1400  35091  bnj1014  35217  bnj1015  35218  bnj1326  35282  bnj1321  35283  bnj1491  35313  fineqvac  35373  mrsubfval  35819  rdgprc0  36102  dfrdg2  36104  brdomaing  36244  fwddifval  36473  fwddifnval  36474  filnetlem4  36702  cureq  38056  ismtyval  38260  isass  38306  isexid  38307  ismgmOLD  38310  elrefrels2  39058  elrefrels3  39059  refreleq  39061  elcnvrefrels2  39074  elcnvrefrels3  39075  elrefsymrels2  39113  eleqvrels2  39136  eleqvrels3  39137  dmqseq  39184  aomclem6  43597  aomclem8  43599  dfac21  43604  tfsconcatun  43875  tfsconcat0b  43884  tfsconcatrev  43886  rclexi  44152  rtrclex  44154  rtrclexi  44158  cnvrcl0  44162  dfrtrcl5  44166  dfrcl2  44211  gneispace2  44669  modelaxreplem1  45515  modelaxreplem2  45516  modelaxrep  45518  ssnnf1octb  45733  sge0val  46901  ismea  46986  caragenval  47028  isome  47029  issmflem  47262  isisubgr  48445  isgrim  48465  fnxpdmdm  48743  elbigo  49134  itcoval  49244  iinfprg  49641  infsubc2  49643  fucofvalne  49907