Theorem dmeq 5891

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 5890	. . 3 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)
2		dmss 5890	. . 3 ⊢ (𝐵 ⊆ 𝐴 → dom 𝐵 ⊆ dom 𝐴)
3	1, 2	anim12i 624	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (dom 𝐴 ⊆ dom 𝐵 ∧ dom 𝐵 ⊆ dom 𝐴))
4		eqss 3960	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
5		eqss 3960	. 2 ⊢ (dom 𝐴 = dom 𝐵 ↔ (dom 𝐴 ⊆ dom 𝐵 ∧ dom 𝐵 ⊆ dom 𝐴))
6	3, 4, 5	3imtr4i 295	1 ⊢ (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567   ⊆ wss 3913  dom cdm 5659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111  df-dm 5669

This theorem is referenced by:  dmeqi  5892  dmeqd  5893  xpid11  5920  resresdm  6231  fneq1  6624  eqfnfv2  7024  funopdmsn  7145  nvof1o  7276  ofrfvalg  7680  offval  7681  offval3  7975  suppval  8154  smoeq  8333  tz7.44lem1  8388  tz7.44-2  8390  tz7.44-3  8391  ereq1  8698  fundmeng  9025  fseqenlem2  10005  dfac3  10101  dfac9  10116  dfac12lem1  10123  dfac12r  10126  ackbij2lem2  10218  ackbij2lem3  10219  r1om  10222  cfsmolem  10250  cfsmo  10251  dcomex  10427  axdc2lem  10428  axdc3lem2  10431  axdc3lem4  10433  ac7g  10454  ttukey2g  10496  fundmge2nop0  14535  s4dom  14952  relexp0g  15055  relexpsucnnr  15058  dfrtrcl2  15095  ello1  15562  elo1  15573  bpolylem  16098  bpolyval  16099  isoval  17818  istsr  18635  ischn  18659  chnind  18673  islindf  21927  decpmatval0  22886  pmatcollpw3lem  22905  ordtval  23311  dfac14  23740  fmval  24065  fmf  24067  blfvalps  24505  tmsval  24603  cfilfval  25388  caufval  25399  isibl  25889  elcpn  26058  bdayval  27774  bdayfo  27803  nosupprefixmo  27826  noinfprefixmo  27827  nosupcbv  27828  nosupdm  27830  nosupfv  27832  nosupres  27833  nosupbnd1lem1  27834  nosupbnd1lem3  27836  nosupbnd1lem5  27838  nosupbnd2  27842  noinfcbv  27843  noinfdm  27845  noinffv  27847  noinfres  27848  noinfbnd1lem3  27851  noinfbnd1lem5  27853  noetasuplem4  27862  noetainflem4  27866  iscgrg  28743  uhgr0e  29358  incistruhgr  29366  ausgrusgri  29455  egrsubgr  29564  vtxdgfval  29754  vtxdg0e  29761  1egrvtxdg1  29796  eupth0  30502  ex-dm  30727  eldmne0  32909  of0r  32961  f1ocnt  33082  tocycfv  33366  tocycf  33374  tocyc01  33375  cycpmco2f1  33381  cycpmco2rn  33382  cycpmco2lem1  33383  cycpmco2lem2  33384  cycpmco2lem3  33385  cycpmco2lem4  33386  cycpmco2lem5  33387  cycpmco2lem6  33388  cycpmco2lem7  33389  cycpmco2  33390  cycpm3cl2  33393  cycpmconjv  33399  tocyccntz  33401  cyc3evpm  33407  cycpmgcl  33410  cycpmconjslem2  33412  cyc3conja  33414  fxpval  33422  locfinreflem  34171  pstmval  34226  cntnevol  34559  omsval  34624  sitgval  34663  elprob  34740  cndprobval  34764  rrvmbfm  34773  bnj1385  35161  bnj1400  35164  bnj1014  35290  bnj1015  35291  bnj1326  35355  bnj1321  35356  bnj1491  35386  fineqvac  35448  mrsubfval  35895  rdgprc0  36178  dfrdg2  36180  brdomaing  36320  fwddifval  36549  fwddifnval  36550  filnetlem4  36777  cureq  38130  ismtyval  38334  isass  38380  isexid  38381  ismgmOLD  38384  elrefrels2  39132  elrefrels3  39133  refreleq  39135  elcnvrefrels2  39148  elcnvrefrels3  39149  elrefsymrels2  39187  eleqvrels2  39210  eleqvrels3  39211  dmqseq  39258  aomclem6  43671  aomclem8  43673  dfac21  43678  tfsconcatun  43949  tfsconcat0b  43958  tfsconcatrev  43960  rclexi  44226  rtrclex  44228  rtrclexi  44232  cnvrcl0  44236  dfrtrcl5  44240  dfrcl2  44285  gneispace2  44743  modelaxreplem1  45572  modelaxreplem2  45573  modelaxrep  45575  ssnnf1octb  45797  sge0val  46965  ismea  47050  caragenval  47092  isome  47093  issmflem  47326  isisubgr  48509  isgrim  48529  fnxpdmdm  48807  elbigo  49209  itcoval  49319  iinfprg  49715  infsubc2  49717  fucofvalne  49981