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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-dm 5634

This theorem is referenced by:  dmeqi  5853  dmeqd  5854  xpid11  5881  resresdm  6191  fneq1  6583  eqfnfv2  6978  funopdmsn  7097  nvof1o  7228  ofrfvalg  7632  offval  7633  offval3  7928  suppval  8105  smoeq  8283  tz7.44lem1  8337  tz7.44-2  8339  tz7.44-3  8340  ereq1  8644  fundmeng  8972  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  21802  decpmatval0  22739  pmatcollpw3lem  22758  ordtval  23164  dfac14  23593  fmval  23918  fmf  23920  blfvalps  24358  tmsval  24456  cfilfval  25241  caufval  25252  isibl  25742  elcpn  25911  bdayval  27626  bdayfo  27655  nosupprefixmo  27678  noinfprefixmo  27679  nosupcbv  27680  nosupdm  27682  nosupfv  27684  nosupres  27685  nosupbnd1lem1  27686  nosupbnd1lem3  27688  nosupbnd1lem5  27690  nosupbnd2  27694  noinfcbv  27695  noinfdm  27697  noinffv  27699  noinfres  27700  noinfbnd1lem3  27703  noinfbnd1lem5  27705  noetasuplem4  27714  noetainflem4  27718  iscgrg  28594  uhgr0e  29154  incistruhgr  29162  ausgrusgri  29251  egrsubgr  29360  vtxdgfval  29551  vtxdg0e  29558  1egrvtxdg1  29593  eupth0  30299  ex-dm  30524  eldmne0  32715  of0r  32767  f1ocnt  32888  tocycfv  33185  tocycf  33193  tocyc01  33194  cycpmco2f1  33200  cycpmco2rn  33201  cycpmco2lem1  33202  cycpmco2lem2  33203  cycpmco2lem3  33204  cycpmco2lem4  33205  cycpmco2lem5  33206  cycpmco2lem6  33207  cycpmco2lem7  33208  cycpmco2  33209  cycpm3cl2  33212  cycpmconjv  33218  tocyccntz  33220  cyc3evpm  33226  cycpmgcl  33229  cycpmconjslem2  33231  cyc3conja  33233  fxpval  33241  locfinreflem  34000  pstmval  34055  cntnevol  34388  omsval  34453  sitgval  34492  elprob  34569  cndprobval  34593  rrvmbfm  34602  bnj1385  34990  bnj1400  34993  bnj1014  35119  bnj1015  35120  bnj1326  35184  bnj1321  35185  bnj1491  35215  fineqvac  35276  mrsubfval  35706  rdgprc0  35989  dfrdg2  35991  brdomaing  36131  fwddifval  36360  fwddifnval  36361  filnetlem4  36579  cureq  37931  ismtyval  38135  isass  38181  isexid  38182  ismgmOLD  38185  elrefrels2  38933  elrefrels3  38934  refreleq  38936  elcnvrefrels2  38949  elcnvrefrels3  38950  elrefsymrels2  38988  eleqvrels2  39011  eleqvrels3  39012  dmqseq  39059  aomclem6  43505  aomclem8  43507  dfac21  43512  tfsconcatun  43783  tfsconcat0b  43792  tfsconcatrev  43794  rclexi  44060  rtrclex  44062  rtrclexi  44066  cnvrcl0  44070  dfrtrcl5  44074  dfrcl2  44119  gneispace2  44577  modelaxreplem1  45423  modelaxreplem2  45424  modelaxrep  45426  ssnnf1octb  45642  sge0val  46812  ismea  46897  caragenval  46939  isome  46940  issmflem  47173  isisubgr  48350  isgrim  48370  fnxpdmdm  48648  elbigo  49039  itcoval  49149  iinfprg  49546  infsubc2  49548  fucofvalne  49812