Theorem dmeq 5867

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ⊆ wss 3914  dom cdm 5638

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-dm 5648

This theorem is referenced by:  dmeqi  5868  dmeqd  5869  xpid11  5896  resresdm  6206  fneq1  6609  eqfnfv2  7004  funopdmsn  7122  nvof1o  7255  ofrfvalg  7661  offval  7662  offval3  7961  suppval  8141  smoeq  8319  tz7.44lem1  8373  tz7.44-2  8375  tz7.44-3  8376  ereq1  8678  fundmeng  9003  fseqenlem2  9978  dfac3  10074  dfac9  10090  dfac12lem1  10097  dfac12r  10100  ackbij2lem2  10192  ackbij2lem3  10193  r1om  10196  cfsmolem  10223  cfsmo  10224  dcomex  10400  axdc2lem  10401  axdc3lem2  10404  axdc3lem4  10406  ac7g  10427  ttukey2g  10469  fundmge2nop0  14467  s4dom  14885  relexp0g  14988  relexpsucnnr  14991  dfrtrcl2  15028  ello1  15481  elo1  15492  bpolylem  16014  bpolyval  16015  isoval  17727  istsr  18542  islindf  21721  decpmatval0  22651  pmatcollpw3lem  22670  ordtval  23076  dfac14  23505  fmval  23830  fmf  23832  blfvalps  24271  tmsval  24369  cfilfval  25164  caufval  25175  isibl  25666  elcpn  25836  bdayval  27560  bdayfo  27589  nosupprefixmo  27612  noinfprefixmo  27613  nosupcbv  27614  nosupdm  27616  nosupfv  27618  nosupres  27619  nosupbnd1lem1  27620  nosupbnd1lem3  27622  nosupbnd1lem5  27624  nosupbnd2  27628  noinfcbv  27629  noinfdm  27631  noinffv  27633  noinfres  27634  noinfbnd1lem3  27637  noinfbnd1lem5  27639  noetasuplem4  27648  noetainflem4  27652  iscgrg  28439  uhgr0e  28998  incistruhgr  29006  ausgrusgri  29095  egrsubgr  29204  vtxdgfval  29395  vtxdg0e  29402  1egrvtxdg1  29437  eupth0  30143  ex-dm  30368  eldmne0  32552  of0r  32602  f1ocnt  32725  ischn  32932  chnind  32937  tocycfv  33066  tocycf  33074  tocyc01  33075  cycpmco2f1  33081  cycpmco2rn  33082  cycpmco2lem1  33083  cycpmco2lem2  33084  cycpmco2lem3  33085  cycpmco2lem4  33086  cycpmco2lem5  33087  cycpmco2lem6  33088  cycpmco2lem7  33089  cycpmco2  33090  cycpm3cl2  33093  cycpmconjv  33099  tocyccntz  33101  cyc3evpm  33107  cycpmgcl  33110  cycpmconjslem2  33112  cyc3conja  33114  fxpval  33122  locfinreflem  33830  pstmval  33885  cntnevol  34218  omsval  34284  sitgval  34323  elprob  34400  cndprobval  34424  rrvmbfm  34433  bnj1385  34822  bnj1400  34825  bnj1014  34951  bnj1015  34952  bnj1326  35016  bnj1321  35017  bnj1491  35047  fineqvac  35087  mrsubfval  35495  rdgprc0  35781  dfrdg2  35783  brdomaing  35923  fwddifval  36150  fwddifnval  36151  filnetlem4  36369  cureq  37590  ismtyval  37794  isass  37840  isexid  37841  ismgmOLD  37844  elrefrels2  38509  elrefrels3  38510  refreleq  38512  elcnvrefrels2  38525  elcnvrefrels3  38526  elrefsymrels2  38560  eleqvrels2  38583  eleqvrels3  38584  dmqseq  38631  aomclem6  43048  aomclem8  43050  dfac21  43055  tfsconcatun  43326  tfsconcat0b  43335  tfsconcatrev  43337  rclexi  43604  rtrclex  43606  rtrclexi  43610  cnvrcl0  43614  dfrtrcl5  43618  dfrcl2  43663  gneispace2  44121  modelaxreplem1  44968  modelaxreplem2  44969  modelaxrep  44971  ssnnf1octb  45188  sge0val  46364  ismea  46449  caragenval  46491  isome  46492  issmflem  46725  isisubgr  47862  isgrim  47882  fnxpdmdm  48148  elbigo  48540  itcoval  48650  iinfprg  49048  infsubc2  49050  fucofvalne  49314