Theorem dmeq 5845

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 5844	. . 3 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)
2		dmss 5844	. . 3 ⊢ (𝐵 ⊆ 𝐴 → dom 𝐵 ⊆ dom 𝐴)
3	1, 2	anim12i 619	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (dom 𝐴 ⊆ dom 𝐵 ∧ dom 𝐵 ⊆ dom 𝐴))
4		eqss 3930	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
5		eqss 3930	. 2 ⊢ (dom 𝐴 = dom 𝐵 ↔ (dom 𝐴 ⊆ dom 𝐵 ∧ dom 𝐵 ⊆ dom 𝐴))
6	3, 4, 5	3imtr4i 293	1 ⊢ (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ⊆ wss 3883  dom cdm 5618

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-dm 5628

This theorem is referenced by:  dmeqi  5846  dmeqd  5847  xpid11  5874  resresdm  6184  fneq1  6576  eqfnfv2  6972  funopdmsn  7093  nvof1o  7224  ofrfvalg  7628  offval  7629  offval3  7924  suppval  8102  smoeq  8280  tz7.44lem1  8334  tz7.44-2  8336  tz7.44-3  8337  ereq1  8641  fundmeng  8969  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  14455  s4dom  14872  relexp0g  14975  relexpsucnnr  14978  dfrtrcl2  15015  ello1  15468  elo1  15479  bpolylem  16004  bpolyval  16005  isoval  17723  istsr  18540  ischn  18564  chnind  18578  islindf  21787  decpmatval0  22747  pmatcollpw3lem  22766  ordtval  23172  dfac14  23601  fmval  23926  fmf  23928  blfvalps  24366  tmsval  24464  cfilfval  25249  caufval  25260  isibl  25750  elcpn  25919  bdayval  27630  bdayfo  27659  nosupprefixmo  27682  noinfprefixmo  27683  nosupcbv  27684  nosupdm  27686  nosupfv  27688  nosupres  27689  nosupbnd1lem1  27690  nosupbnd1lem3  27692  nosupbnd1lem5  27694  nosupbnd2  27698  noinfcbv  27699  noinfdm  27701  noinffv  27703  noinfres  27704  noinfbnd1lem3  27707  noinfbnd1lem5  27709  noetasuplem4  27718  noetainflem4  27722  iscgrg  28598  uhgr0e  29158  incistruhgr  29166  ausgrusgri  29255  egrsubgr  29364  vtxdgfval  29554  vtxdg0e  29561  1egrvtxdg1  29596  eupth0  30302  ex-dm  30527  eldmne0  32719  of0r  32771  f1ocnt  32892  tocycfv  33190  tocycf  33198  tocyc01  33199  cycpmco2f1  33205  cycpmco2rn  33206  cycpmco2lem1  33207  cycpmco2lem2  33208  cycpmco2lem3  33209  cycpmco2lem4  33210  cycpmco2lem5  33211  cycpmco2lem6  33212  cycpmco2lem7  33213  cycpmco2  33214  cycpm3cl2  33217  cycpmconjv  33223  tocyccntz  33225  cyc3evpm  33231  cycpmgcl  33234  cycpmconjslem2  33236  cyc3conja  33238  fxpval  33246  locfinreflem  34024  pstmval  34079  cntnevol  34412  omsval  34477  sitgval  34516  elprob  34593  cndprobval  34617  rrvmbfm  34626  bnj1385  35014  bnj1400  35017  bnj1014  35143  bnj1015  35144  bnj1326  35208  bnj1321  35209  bnj1491  35239  fineqvac  35297  mrsubfval  35736  rdgprc0  36019  dfrdg2  36021  brdomaing  36161  fwddifval  36390  fwddifnval  36391  filnetlem4  36609  cureq  37963  ismtyval  38167  isass  38213  isexid  38214  ismgmOLD  38217  elrefrels2  38965  elrefrels3  38966  refreleq  38968  elcnvrefrels2  38981  elcnvrefrels3  38982  elrefsymrels2  39020  eleqvrels2  39043  eleqvrels3  39044  dmqseq  39091  aomclem6  43504  aomclem8  43506  dfac21  43511  tfsconcatun  43782  tfsconcat0b  43791  tfsconcatrev  43793  rclexi  44059  rtrclex  44061  rtrclexi  44065  cnvrcl0  44069  dfrtrcl5  44073  dfrcl2  44118  gneispace2  44576  modelaxreplem1  45422  modelaxreplem2  45423  modelaxrep  45425  ssnnf1octb  45641  sge0val  46809  ismea  46894  caragenval  46936  isome  46937  issmflem  47170  isisubgr  48353  isgrim  48373  fnxpdmdm  48651  elbigo  49042  itcoval  49152  iinfprg  49549  infsubc2  49551  fucofvalne  49815