Theorem dmeq 5917

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ⊆ wss 3963  dom cdm 5689

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-dm 5699

This theorem is referenced by:  dmeqi  5918  dmeqd  5919  xpid11  5946  resresdm  6255  fneq1  6660  eqfnfv2  7052  funopdmsn  7170  nvof1o  7300  ofrfvalg  7705  offval  7706  offval3  8006  suppval  8186  smoeq  8389  tz7.44lem1  8444  tz7.44-2  8446  tz7.44-3  8447  ereq1  8751  fundmeng  9071  fseqenlem2  10063  dfac3  10159  dfac9  10175  dfac12lem1  10182  dfac12r  10185  ackbij2lem2  10277  ackbij2lem3  10278  r1om  10281  cfsmolem  10308  cfsmo  10309  dcomex  10485  axdc2lem  10486  axdc3lem2  10489  axdc3lem4  10491  ac7g  10512  ttukey2g  10554  fundmge2nop0  14538  s4dom  14955  relexp0g  15058  relexpsucnnr  15061  dfrtrcl2  15098  ello1  15548  elo1  15559  bpolylem  16081  bpolyval  16082  isoval  17813  istsr  18641  islindf  21850  decpmatval0  22786  pmatcollpw3lem  22805  ordtval  23213  dfac14  23642  fmval  23967  fmf  23969  blfvalps  24409  tmsval  24509  cfilfval  25312  caufval  25323  isibl  25815  elcpn  25985  bdayval  27708  bdayfo  27737  nosupprefixmo  27760  noinfprefixmo  27761  nosupcbv  27762  nosupdm  27764  nosupfv  27766  nosupres  27767  nosupbnd1lem1  27768  nosupbnd1lem3  27770  nosupbnd1lem5  27772  nosupbnd2  27776  noinfcbv  27777  noinfdm  27779  noinffv  27781  noinfres  27782  noinfbnd1lem3  27785  noinfbnd1lem5  27787  noetasuplem4  27796  noetainflem4  27800  iscgrg  28535  uhgr0e  29103  incistruhgr  29111  ausgrusgri  29200  egrsubgr  29309  vtxdgfval  29500  vtxdg0e  29507  1egrvtxdg1  29542  eupth0  30243  ex-dm  30468  eldmne0  32645  of0r  32695  f1ocnt  32810  ischn  32981  chnind  32985  tocycfv  33112  tocycf  33120  tocyc01  33121  cycpmco2f1  33127  cycpmco2rn  33128  cycpmco2lem1  33129  cycpmco2lem2  33130  cycpmco2lem3  33131  cycpmco2lem4  33132  cycpmco2lem5  33133  cycpmco2lem6  33134  cycpmco2lem7  33135  cycpmco2  33136  cycpm3cl2  33139  cycpmconjv  33145  tocyccntz  33147  cyc3evpm  33153  cycpmgcl  33156  cycpmconjslem2  33158  cyc3conja  33160  locfinreflem  33801  pstmval  33856  cntnevol  34209  omsval  34275  sitgval  34314  elprob  34391  cndprobval  34415  rrvmbfm  34424  bnj1385  34825  bnj1400  34828  bnj1014  34954  bnj1015  34955  bnj1326  35019  bnj1321  35020  bnj1491  35050  fineqvac  35090  mrsubfval  35493  rdgprc0  35775  dfrdg2  35777  brdomaing  35917  fwddifval  36144  fwddifnval  36145  filnetlem4  36364  cureq  37583  ismtyval  37787  isass  37833  isexid  37834  ismgmOLD  37837  elrefrels2  38500  elrefrels3  38501  refreleq  38503  elcnvrefrels2  38516  elcnvrefrels3  38517  elrefsymrels2  38551  eleqvrels2  38574  eleqvrels3  38575  dmqseq  38622  aomclem6  43048  aomclem8  43050  dfac21  43055  tfsconcatun  43327  tfsconcat0b  43336  tfsconcatrev  43338  rclexi  43605  rtrclex  43607  rtrclexi  43611  cnvrcl0  43615  dfrtrcl5  43619  dfrcl2  43664  gneispace2  44122  modelaxreplem1  44943  modelaxreplem2  44944  modelaxrep  44946  ssnnf1octb  45137  sge0val  46322  ismea  46407  caragenval  46449  isome  46450  issmflem  46683  isisubgr  47786  isgrim  47806  fnxpdmdm  48004  elbigo  48401  itcoval  48511