Theorem dmeq 5757

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1543   ⊆ wss 3853  dom cdm 5536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-rab 3060  df-v 3400  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-br 5040  df-dm 5546

This theorem is referenced by:  dmeqi  5758  dmeqd  5759  xpid11  5786  resresdm  6076  fneq1  6448  eqfnfv2  6831  funopdmsn  6943  nvof1o  7069  ofrfvalg  7454  offval  7455  offval3  7733  suppval  7883  smoeq  8065  tz7.44lem1  8119  tz7.44-2  8121  tz7.44-3  8122  ereq1  8376  fundmeng  8687  fseqenlem2  9604  dfac3  9700  dfac9  9715  dfac12lem1  9722  dfac12r  9725  ackbij2lem2  9819  ackbij2lem3  9820  r1om  9823  cfsmolem  9849  cfsmo  9850  dcomex  10026  axdc2lem  10027  axdc3lem2  10030  axdc3lem4  10032  ac7g  10053  ttukey2g  10095  fundmge2nop0  14023  s4dom  14449  relexp0g  14550  relexpsucnnr  14553  dfrtrcl2  14590  ello1  15041  elo1  15052  bpolylem  15573  bpolyval  15574  isoval  17224  istsr  18043  islindf  20728  decpmatval0  21615  pmatcollpw3lem  21634  ordtval  22040  dfac14  22469  fmval  22794  fmf  22796  blfvalps  23235  tmsval  23333  cfilfval  24115  caufval  24126  isibl  24617  elcpn  24785  iscgrg  26557  uhgr0e  27116  incistruhgr  27124  ausgrusgri  27213  egrsubgr  27319  vtxdgfval  27509  vtxdg0e  27516  1egrvtxdg1  27551  eupth0  28251  ex-dm  28476  eldmne0  30636  f1ocnt  30797  tocycfv  31049  tocycf  31057  tocyc01  31058  cycpmco2f1  31064  cycpmco2rn  31065  cycpmco2lem1  31066  cycpmco2lem2  31067  cycpmco2lem3  31068  cycpmco2lem4  31069  cycpmco2lem5  31070  cycpmco2lem6  31071  cycpmco2lem7  31072  cycpmco2  31073  cycpm3cl2  31076  cycpmconjv  31082  tocyccntz  31084  cyc3evpm  31090  cycpmgcl  31093  cycpmconjslem2  31095  cyc3conja  31097  locfinreflem  31458  pstmval  31513  cntnevol  31862  omsval  31926  sitgval  31965  elprob  32042  cndprobval  32066  rrvmbfm  32075  bnj1385  32479  bnj1400  32482  bnj1014  32608  bnj1015  32609  bnj1326  32673  bnj1321  32674  bnj1491  32704  fineqvac  32733  mrsubfval  33137  rdgprc0  33439  dfrdg2  33441  bdayval  33537  bdayfo  33566  nosupprefixmo  33589  noinfprefixmo  33590  nosupcbv  33591  nosupdm  33593  nosupfv  33595  nosupres  33596  nosupbnd1lem1  33597  nosupbnd1lem3  33599  nosupbnd1lem5  33601  nosupbnd2  33605  noinfcbv  33606  noinfdm  33608  noinffv  33610  noinfres  33611  noinfbnd1lem3  33614  noinfbnd1lem5  33616  noetasuplem4  33625  noetainflem4  33629  brdomaing  33923  fwddifval  34150  fwddifnval  34151  filnetlem4  34256  cureq  35439  ismtyval  35644  isass  35690  isexid  35691  ismgmOLD  35694  elrefrels2  36321  elrefrels3  36322  refreleq  36324  elcnvrefrels2  36334  elcnvrefrels3  36335  elrefsymrels2  36369  eleqvrels2  36391  eleqvrels3  36392  dmqseq  36439  aomclem6  40528  aomclem8  40530  dfac21  40535  rclexi  40840  rtrclex  40842  rtrclexi  40846  cnvrcl0  40850  dfrtrcl5  40854  dfrcl2  40900  gneispace2  41360  ssnnf1octb  42347  sge0val  43522  ismea  43607  caragenval  43649  isome  43650  issmflem  43878  isomgreqve  44893  fnxpdmdm  44938  elbigo  45513  itcoval  45623