Theorem dmeq 5884

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 5883	. . 3 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)
2		dmss 5883	. . 3 ⊢ (𝐵 ⊆ 𝐴 → dom 𝐵 ⊆ dom 𝐴)
3	1, 2	anim12i 625	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (dom 𝐴 ⊆ dom 𝐵 ∧ dom 𝐵 ⊆ dom 𝐴))
4		eqss 3923	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
5		eqss 3923	. 2 ⊢ (dom 𝐴 = dom 𝐵 ↔ (dom 𝐴 ⊆ dom 𝐵 ∧ dom 𝐵 ⊆ dom 𝐴))
6	3, 4, 5	3imtr4i 295	1 ⊢ (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ⊆ wss 3895  dom cdm 5650

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-dm 5660

This theorem is used by:  dmeqi  5885  dmeqd  5886  xpid11  5913  resresdm  6234  fneq1  6631  eqfnfv2  7031  funopdmsn  7155  nvof1o  7289  ofrfvalg  7702  offval  7703  offval3  7995  suppval  8182  smoeq  8362  tz7.44lem1  8417  tz7.44-2  8419  tz7.44-3  8420  ereq1  8729  cureq  8893  fundmeng  9064  fseqenlem2  10108  dfac3  10204  dfac9  10219  dfac12lem1  10226  dfac12r  10229  ackbij2lem2  10321  ackbij2lem3  10322  hfom  10325  cfsmolem  10352  cfsmo  10353  dcomex  10529  axdc2lem  10530  axdc3lem2  10533  axdc3lem4  10535  ac7g  10556  ttukey2g  10598  fundmge2nop0  14651  s4dom  15076  relexp0g  15181  relexpsucnnr  15184  dfrtrcl2  15221  ello1  15688  elo1  15699  bpolylem  16220  bpolyval  16221  isoval  17946  istsr  18763  ischn  18787  chnind  18801  islindf  22124  decpmatval0  23088  pmatcollpw3lem  23107  ordtval  23513  dfac14  23943  fmval  24268  fmf  24270  blfvalps  24708  tmsval  24806  cfilfval  25591  caufval  25602  isibl  26092  elcpn  26260  bdayval  28011  bdayfo  28040  nosupprefixmo  28063  noinfprefixmo  28064  nosupcbv  28065  nosupdm  28067  nosupfv  28069  nosupres  28070  nosupbnd1lem1  28071  nosupbnd1lem3  28073  nosupbnd1lem5  28075  nosupbnd2  28079  noinfcbv  28080  noinfdm  28082  noinffv  28084  noinfres  28085  noinfbnd1lem3  28088  noinfbnd1lem5  28090  noetasuplem4  28099  noetainflem4  28103  iscgrg  28981  uhgr0e  29655  incistruhgr  29663  ausgrusgri  29755  egrsubgr  29864  vtxdgfval  30054  vtxdg0e  30061  1egrvtxdg1  30096  eupth0  30821  ex-dm  31046  eldmne0  33269  of0r  33321  f1ocnt  33439  tocycfv  33717  tocycf  33725  tocyc01  33726  cycpmco2f1  33732  cycpmco2rn  33733  cycpmco2lem1  33734  cycpmco2lem2  33735  cycpmco2lem3  33736  cycpmco2lem4  33737  cycpmco2lem5  33738  cycpmco2lem6  33739  cycpmco2lem7  33740  cycpmco2  33741  cycpm3cl2  33744  cycpmconjv  33750  tocyccntz  33752  cyc3evpm  33758  cycpmgcl  33761  cycpmconjslem2  33763  cyc3conja  33765  fxpval  33773  locfinreflem  34519  pstmval  34574  cntnevol  34908  omsval  34972  sitgval  35011  elprob  35088  cndprobval  35112  rrvmbfm  35121  bnj1385  35509  bnj1400  35512  bnj1014  35638  bnj1015  35639  bnj1326  35703  bnj1321  35704  bnj1491  35734  fineqvac  35841  srepdflem2  36006  srepdf  36007  mrsubfval  36360  rdgprc0  36648  dfrdg2  36650  brdomaing  36790  fwddifval  37020  fwddifnval  37021  filnetlem4  37262  ismtyval  38828  isass  38874  isexid  38875  ismgmOLD  38878  elrefrels2  39624  elrefrels3  39625  refreleq  39627  elcnvrefrels2  39640  elcnvrefrels3  39641  elrefsymrels2  39679  eleqvrels2  39702  eleqvrels3  39703  dmqseq  39750  aomclem6  44155  aomclem8  44157  dfac21  44162  tfsconcatun  44433  tfsconcat0b  44442  tfsconcatrev  44444  rclexi  44709  rtrclex  44711  rtrclexi  44715  cnvrcl0  44719  dfrtrcl5  44723  dfrcl2  44768  gneispace2  45226  modelaxreplem1  46062  modelaxreplem2  46063  modelaxrep  46065  ssnnf1octb  46303  sge0val  47470  ismea  47555  caragenval  47597  isome  47598  issmflem  47831  isisubgr  49054  isgrim  49074  fnxpdmdm  49351  elbigo  49757  itcoval  49867  iinfprg  50267  infsubc2  50269  fucofvalne  50541