Theorem dmeq 5852

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ⊆ wss 3901  dom cdm 5624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-dm 5634

This theorem is referenced by:  dmeqi  5853  dmeqd  5854  xpid11  5881  resresdm  6191  fneq1  6583  eqfnfv2  6977  funopdmsn  7095  nvof1o  7226  ofrfvalg  7630  offval  7631  offval3  7926  suppval  8104  smoeq  8282  tz7.44lem1  8336  tz7.44-2  8338  tz7.44-3  8339  ereq1  8642  fundmeng  8969  fseqenlem2  9935  dfac3  10031  dfac9  10047  dfac12lem1  10054  dfac12r  10057  ackbij2lem2  10149  ackbij2lem3  10150  r1om  10153  cfsmolem  10180  cfsmo  10181  dcomex  10357  axdc2lem  10358  axdc3lem2  10361  axdc3lem4  10363  ac7g  10384  ttukey2g  10426  fundmge2nop0  14425  s4dom  14842  relexp0g  14945  relexpsucnnr  14948  dfrtrcl2  14985  ello1  15438  elo1  15449  bpolylem  15971  bpolyval  15972  isoval  17689  istsr  18506  ischn  18530  chnind  18544  islindf  21767  decpmatval0  22708  pmatcollpw3lem  22727  ordtval  23133  dfac14  23562  fmval  23887  fmf  23889  blfvalps  24327  tmsval  24425  cfilfval  25220  caufval  25231  isibl  25722  elcpn  25892  bdayval  27616  bdayfo  27645  nosupprefixmo  27668  noinfprefixmo  27669  nosupcbv  27670  nosupdm  27672  nosupfv  27674  nosupres  27675  nosupbnd1lem1  27676  nosupbnd1lem3  27678  nosupbnd1lem5  27680  nosupbnd2  27684  noinfcbv  27685  noinfdm  27687  noinffv  27689  noinfres  27690  noinfbnd1lem3  27693  noinfbnd1lem5  27695  noetasuplem4  27704  noetainflem4  27708  iscgrg  28584  uhgr0e  29144  incistruhgr  29152  ausgrusgri  29241  egrsubgr  29350  vtxdgfval  29541  vtxdg0e  29548  1egrvtxdg1  29583  eupth0  30289  ex-dm  30514  eldmne0  32705  of0r  32758  f1ocnt  32880  tocycfv  33191  tocycf  33199  tocyc01  33200  cycpmco2f1  33206  cycpmco2rn  33207  cycpmco2lem1  33208  cycpmco2lem2  33209  cycpmco2lem3  33210  cycpmco2lem4  33211  cycpmco2lem5  33212  cycpmco2lem6  33213  cycpmco2lem7  33214  cycpmco2  33215  cycpm3cl2  33218  cycpmconjv  33224  tocyccntz  33226  cyc3evpm  33232  cycpmgcl  33235  cycpmconjslem2  33237  cyc3conja  33239  fxpval  33247  locfinreflem  33997  pstmval  34052  cntnevol  34385  omsval  34450  sitgval  34489  elprob  34566  cndprobval  34590  rrvmbfm  34599  bnj1385  34988  bnj1400  34991  bnj1014  35117  bnj1015  35118  bnj1326  35182  bnj1321  35183  bnj1491  35213  fineqvac  35272  mrsubfval  35702  rdgprc0  35985  dfrdg2  35987  brdomaing  36127  fwddifval  36356  fwddifnval  36357  filnetlem4  36575  cureq  37797  ismtyval  38001  isass  38047  isexid  38048  ismgmOLD  38051  elrefrels2  38771  elrefrels3  38772  refreleq  38774  elcnvrefrels2  38787  elcnvrefrels3  38788  elrefsymrels2  38826  eleqvrels2  38849  eleqvrels3  38850  dmqseq  38898  aomclem6  43301  aomclem8  43303  dfac21  43308  tfsconcatun  43579  tfsconcat0b  43588  tfsconcatrev  43590  rclexi  43856  rtrclex  43858  rtrclexi  43862  cnvrcl0  43866  dfrtrcl5  43870  dfrcl2  43915  gneispace2  44373  modelaxreplem1  45219  modelaxreplem2  45220  modelaxrep  45222  ssnnf1octb  45438  sge0val  46610  ismea  46695  caragenval  46737  isome  46738  issmflem  46971  isisubgr  48108  isgrim  48128  fnxpdmdm  48406  elbigo  48797  itcoval  48907  iinfprg  49304  infsubc2  49306  fucofvalne  49570