Theorem dmeq 5809

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 5808	. . 3 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)
2		dmss 5808	. . 3 ⊢ (𝐵 ⊆ 𝐴 → dom 𝐵 ⊆ dom 𝐴)
3	1, 2	anim12i 612	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (dom 𝐴 ⊆ dom 𝐵 ∧ dom 𝐵 ⊆ dom 𝐴))
4		eqss 3940	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
5		eqss 3940	. 2 ⊢ (dom 𝐴 = dom 𝐵 ↔ (dom 𝐴 ⊆ dom 𝐵 ∧ dom 𝐵 ⊆ dom 𝐴))
6	3, 4, 5	3imtr4i 291	1 ⊢ (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-br 5079  df-dm 5598

This theorem is referenced by:  dmeqi  5810  dmeqd  5811  xpid11  5838  resresdm  6133  fneq1  6520  eqfnfv2  6904  funopdmsn  7016  nvof1o  7146  ofrfvalg  7532  offval  7533  offval3  7811  suppval  7963  smoeq  8165  tz7.44lem1  8220  tz7.44-2  8222  tz7.44-3  8223  ereq1  8479  fundmeng  8792  fseqenlem2  9765  dfac3  9861  dfac9  9876  dfac12lem1  9883  dfac12r  9886  ackbij2lem2  9980  ackbij2lem3  9981  r1om  9984  cfsmolem  10010  cfsmo  10011  dcomex  10187  axdc2lem  10188  axdc3lem2  10191  axdc3lem4  10193  ac7g  10214  ttukey2g  10256  fundmge2nop0  14187  s4dom  14613  relexp0g  14714  relexpsucnnr  14717  dfrtrcl2  14754  ello1  15205  elo1  15216  bpolylem  15739  bpolyval  15740  isoval  17458  istsr  18282  islindf  21000  decpmatval0  21894  pmatcollpw3lem  21913  ordtval  22321  dfac14  22750  fmval  23075  fmf  23077  blfvalps  23517  tmsval  23617  cfilfval  24409  caufval  24420  isibl  24911  elcpn  25079  iscgrg  26854  uhgr0e  27422  incistruhgr  27430  ausgrusgri  27519  egrsubgr  27625  vtxdgfval  27815  vtxdg0e  27822  1egrvtxdg1  27857  eupth0  28557  ex-dm  28782  eldmne0  30942  f1ocnt  31102  tocycfv  31355  tocycf  31363  tocyc01  31364  cycpmco2f1  31370  cycpmco2rn  31371  cycpmco2lem1  31372  cycpmco2lem2  31373  cycpmco2lem3  31374  cycpmco2lem4  31375  cycpmco2lem5  31376  cycpmco2lem6  31377  cycpmco2lem7  31378  cycpmco2  31379  cycpm3cl2  31382  cycpmconjv  31388  tocyccntz  31390  cyc3evpm  31396  cycpmgcl  31399  cycpmconjslem2  31401  cyc3conja  31403  locfinreflem  31769  pstmval  31824  cntnevol  32175  omsval  32239  sitgval  32278  elprob  32355  cndprobval  32379  rrvmbfm  32388  bnj1385  32791  bnj1400  32794  bnj1014  32920  bnj1015  32921  bnj1326  32985  bnj1321  32986  bnj1491  33016  fineqvac  33045  mrsubfval  33449  rdgprc0  33748  dfrdg2  33750  bdayval  33830  bdayfo  33859  nosupprefixmo  33882  noinfprefixmo  33883  nosupcbv  33884  nosupdm  33886  nosupfv  33888  nosupres  33889  nosupbnd1lem1  33890  nosupbnd1lem3  33892  nosupbnd1lem5  33894  nosupbnd2  33898  noinfcbv  33899  noinfdm  33901  noinffv  33903  noinfres  33904  noinfbnd1lem3  33907  noinfbnd1lem5  33909  noetasuplem4  33918  noetainflem4  33922  brdomaing  34216  fwddifval  34443  fwddifnval  34444  filnetlem4  34549  cureq  35732  ismtyval  35937  isass  35983  isexid  35984  ismgmOLD  35987  elrefrels2  36614  elrefrels3  36615  refreleq  36617  elcnvrefrels2  36627  elcnvrefrels3  36628  elrefsymrels2  36662  eleqvrels2  36684  eleqvrels3  36685  dmqseq  36732  aomclem6  40864  aomclem8  40866  dfac21  40871  rclexi  41176  rtrclex  41178  rtrclexi  41182  cnvrcl0  41186  dfrtrcl5  41190  dfrcl2  41235  gneispace2  41695  ssnnf1octb  42686  sge0val  43858  ismea  43943  caragenval  43985  isome  43986  issmflem  44214  isomgreqve  45229  fnxpdmdm  45274  elbigo  45849  itcoval  45959