Theorem dmeq 5850

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 5849	. . 3 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)
2		dmss 5849	. . 3 ⊢ (𝐵 ⊆ 𝐴 → dom 𝐵 ⊆ dom 𝐴)
3	1, 2	anim12i 613	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (dom 𝐴 ⊆ dom 𝐵 ∧ dom 𝐵 ⊆ dom 𝐴))
4		eqss 3953	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
5		eqss 3953	. 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 3905  dom cdm 5623

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 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-dm 5633

This theorem is referenced by:  dmeqi  5851  dmeqd  5852  xpid11  5878  resresdm  6186  fneq1  6577  eqfnfv2  6970  funopdmsn  7088  nvof1o  7221  ofrfvalg  7625  offval  7626  offval3  7924  suppval  8102  smoeq  8280  tz7.44lem1  8334  tz7.44-2  8336  tz7.44-3  8337  ereq1  8639  fundmeng  8964  fseqenlem2  9938  dfac3  10034  dfac9  10050  dfac12lem1  10057  dfac12r  10060  ackbij2lem2  10152  ackbij2lem3  10153  r1om  10156  cfsmolem  10183  cfsmo  10184  dcomex  10360  axdc2lem  10361  axdc3lem2  10364  axdc3lem4  10366  ac7g  10387  ttukey2g  10429  fundmge2nop0  14427  s4dom  14844  relexp0g  14947  relexpsucnnr  14950  dfrtrcl2  14987  ello1  15440  elo1  15451  bpolylem  15973  bpolyval  15974  isoval  17690  istsr  18507  islindf  21737  decpmatval0  22667  pmatcollpw3lem  22686  ordtval  23092  dfac14  23521  fmval  23846  fmf  23848  blfvalps  24287  tmsval  24385  cfilfval  25180  caufval  25191  isibl  25682  elcpn  25852  bdayval  27576  bdayfo  27605  nosupprefixmo  27628  noinfprefixmo  27629  nosupcbv  27630  nosupdm  27632  nosupfv  27634  nosupres  27635  nosupbnd1lem1  27636  nosupbnd1lem3  27638  nosupbnd1lem5  27640  nosupbnd2  27644  noinfcbv  27645  noinfdm  27647  noinffv  27649  noinfres  27650  noinfbnd1lem3  27653  noinfbnd1lem5  27655  noetasuplem4  27664  noetainflem4  27668  iscgrg  28475  uhgr0e  29034  incistruhgr  29042  ausgrusgri  29131  egrsubgr  29240  vtxdgfval  29431  vtxdg0e  29438  1egrvtxdg1  29473  eupth0  30176  ex-dm  30401  eldmne0  32585  of0r  32635  f1ocnt  32758  ischn  32961  chnind  32966  tocycfv  33064  tocycf  33072  tocyc01  33073  cycpmco2f1  33079  cycpmco2rn  33080  cycpmco2lem1  33081  cycpmco2lem2  33082  cycpmco2lem3  33083  cycpmco2lem4  33084  cycpmco2lem5  33085  cycpmco2lem6  33086  cycpmco2lem7  33087  cycpmco2  33088  cycpm3cl2  33091  cycpmconjv  33097  tocyccntz  33099  cyc3evpm  33105  cycpmgcl  33108  cycpmconjslem2  33110  cyc3conja  33112  fxpval  33120  locfinreflem  33809  pstmval  33864  cntnevol  34197  omsval  34263  sitgval  34302  elprob  34379  cndprobval  34403  rrvmbfm  34412  bnj1385  34801  bnj1400  34804  bnj1014  34930  bnj1015  34931  bnj1326  34995  bnj1321  34996  bnj1491  35026  fineqvac  35074  mrsubfval  35483  rdgprc0  35769  dfrdg2  35771  brdomaing  35911  fwddifval  36138  fwddifnval  36139  filnetlem4  36357  cureq  37578  ismtyval  37782  isass  37828  isexid  37829  ismgmOLD  37832  elrefrels2  38497  elrefrels3  38498  refreleq  38500  elcnvrefrels2  38513  elcnvrefrels3  38514  elrefsymrels2  38548  eleqvrels2  38571  eleqvrels3  38572  dmqseq  38619  aomclem6  43035  aomclem8  43037  dfac21  43042  tfsconcatun  43313  tfsconcat0b  43322  tfsconcatrev  43324  rclexi  43591  rtrclex  43593  rtrclexi  43597  cnvrcl0  43601  dfrtrcl5  43605  dfrcl2  43650  gneispace2  44108  modelaxreplem1  44955  modelaxreplem2  44956  modelaxrep  44958  ssnnf1octb  45175  sge0val  46351  ismea  46436  caragenval  46478  isome  46479  issmflem  46712  isisubgr  47850  isgrim  47870  fnxpdmdm  48148  elbigo  48540  itcoval  48650  iinfprg  49048  infsubc2  49050  fucofvalne  49314