Theorem dmeq 5887

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ⊆ wss 3899  dom cdm 5655

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-dm 5665

This theorem is used by:  dmeqi  5888  dmeqd  5889  xpid11  5916  resresdm  6229  fneq1  6623  eqfnfv2  7023  funopdmsn  7147  nvof1o  7281  ofrfvalg  7686  offval  7687  offval3  7979  suppval  8160  smoeq  8339  tz7.44lem1  8394  tz7.44-2  8396  tz7.44-3  8397  ereq1  8704  cureq  8868  fundmeng  9039  fseqenlem2  10028  dfac3  10124  dfac9  10139  dfac12lem1  10146  dfac12r  10149  ackbij2lem2  10241  ackbij2lem3  10242  r1om  10245  cfsmolem  10272  cfsmo  10273  dcomex  10449  axdc2lem  10450  axdc3lem2  10453  axdc3lem4  10455  ac7g  10476  ttukey2g  10518  fundmge2nop0  14567  s4dom  14990  relexp0g  15095  relexpsucnnr  15098  dfrtrcl2  15135  ello1  15602  elo1  15613  bpolylem  16134  bpolyval  16135  isoval  17854  istsr  18671  ischn  18695  chnind  18709  islindf  22025  decpmatval0  22989  pmatcollpw3lem  23008  ordtval  23414  dfac14  23844  fmval  24169  fmf  24171  blfvalps  24609  tmsval  24707  cfilfval  25492  caufval  25503  isibl  25993  elcpn  26161  bdayval  27884  bdayfo  27913  nosupprefixmo  27936  noinfprefixmo  27937  nosupcbv  27938  nosupdm  27940  nosupfv  27942  nosupres  27943  nosupbnd1lem1  27944  nosupbnd1lem3  27946  nosupbnd1lem5  27948  nosupbnd2  27952  noinfcbv  27953  noinfdm  27955  noinffv  27957  noinfres  27958  noinfbnd1lem3  27961  noinfbnd1lem5  27963  noetasuplem4  27972  noetainflem4  27976  iscgrg  28854  uhgr0e  29528  incistruhgr  29536  ausgrusgri  29628  egrsubgr  29737  vtxdgfval  29927  vtxdg0e  29934  1egrvtxdg1  29969  eupth0  30694  ex-dm  30919  eldmne0  33100  of0r  33152  f1ocnt  33271  tocycfv  33549  tocycf  33557  tocyc01  33558  cycpmco2f1  33564  cycpmco2rn  33565  cycpmco2lem1  33566  cycpmco2lem2  33567  cycpmco2lem3  33568  cycpmco2lem4  33569  cycpmco2lem5  33570  cycpmco2lem6  33571  cycpmco2lem7  33572  cycpmco2  33573  cycpm3cl2  33576  cycpmconjv  33582  tocyccntz  33584  cyc3evpm  33590  cycpmgcl  33593  cycpmconjslem2  33595  cyc3conja  33597  fxpval  33605  locfinreflem  34350  pstmval  34405  cntnevol  34739  omsval  34804  sitgval  34843  elprob  34920  cndprobval  34944  rrvmbfm  34953  bnj1385  35341  bnj1400  35344  bnj1014  35470  bnj1015  35471  bnj1326  35535  bnj1321  35536  bnj1491  35566  fineqvac  35642  mrsubfval  36087  rdgprc0  36370  dfrdg2  36372  brdomaing  36512  fwddifval  36742  fwddifnval  36743  filnetlem4  37000  ismtyval  38550  isass  38596  isexid  38597  ismgmOLD  38600  elrefrels2  39346  elrefrels3  39347  refreleq  39349  elcnvrefrels2  39362  elcnvrefrels3  39363  elrefsymrels2  39401  eleqvrels2  39424  eleqvrels3  39425  dmqseq  39472  aomclem6  43900  aomclem8  43902  dfac21  43907  tfsconcatun  44178  tfsconcat0b  44187  tfsconcatrev  44189  rclexi  44455  rtrclex  44457  rtrclexi  44461  cnvrcl0  44465  dfrtrcl5  44469  dfrcl2  44514  gneispace2  44972  modelaxreplem1  45801  modelaxreplem2  45802  modelaxrep  45804  ssnnf1octb  46026  sge0val  47194  ismea  47279  caragenval  47321  isome  47322  issmflem  47555  isisubgr  48778  isgrim  48798  fnxpdmdm  49075  elbigo  49481  itcoval  49591  iinfprg  49985  infsubc2  49987  fucofvalne  50251