Theorem dmeq 5858

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 5857	. . 3 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)
2		dmss 5857	. . 3 ⊢ (𝐵 ⊆ 𝐴 → dom 𝐵 ⊆ dom 𝐴)
3	1, 2	anim12i 614	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (dom 𝐴 ⊆ dom 𝐵 ∧ dom 𝐵 ⊆ dom 𝐴))
4		eqss 3937	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
5		eqss 3937	. 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 3889  dom cdm 5631

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-dm 5641

This theorem is referenced by:  dmeqi  5859  dmeqd  5860  xpid11  5887  resresdm  6197  fneq1  6589  eqfnfv2  6984  funopdmsn  7104  nvof1o  7235  ofrfvalg  7639  offval  7640  offval3  7935  suppval  8112  smoeq  8290  tz7.44lem1  8344  tz7.44-2  8346  tz7.44-3  8347  ereq1  8651  fundmeng  8979  fseqenlem2  9947  dfac3  10043  dfac9  10059  dfac12lem1  10066  dfac12r  10069  ackbij2lem2  10161  ackbij2lem3  10162  r1om  10165  cfsmolem  10192  cfsmo  10193  dcomex  10369  axdc2lem  10370  axdc3lem2  10373  axdc3lem4  10375  ac7g  10396  ttukey2g  10438  fundmge2nop0  14464  s4dom  14881  relexp0g  14984  relexpsucnnr  14987  dfrtrcl2  15024  ello1  15477  elo1  15488  bpolylem  16013  bpolyval  16014  isoval  17732  istsr  18549  ischn  18573  chnind  18587  islindf  21792  decpmatval0  22729  pmatcollpw3lem  22748  ordtval  23154  dfac14  23583  fmval  23908  fmf  23910  blfvalps  24348  tmsval  24446  cfilfval  25231  caufval  25242  isibl  25732  elcpn  25901  bdayval  27612  bdayfo  27641  nosupprefixmo  27664  noinfprefixmo  27665  nosupcbv  27666  nosupdm  27668  nosupfv  27670  nosupres  27671  nosupbnd1lem1  27672  nosupbnd1lem3  27674  nosupbnd1lem5  27676  nosupbnd2  27680  noinfcbv  27681  noinfdm  27683  noinffv  27685  noinfres  27686  noinfbnd1lem3  27689  noinfbnd1lem5  27691  noetasuplem4  27700  noetainflem4  27704  iscgrg  28580  uhgr0e  29140  incistruhgr  29148  ausgrusgri  29237  egrsubgr  29346  vtxdgfval  29536  vtxdg0e  29543  1egrvtxdg1  29578  eupth0  30284  ex-dm  30509  eldmne0  32700  of0r  32752  f1ocnt  32873  tocycfv  33170  tocycf  33178  tocyc01  33179  cycpmco2f1  33185  cycpmco2rn  33186  cycpmco2lem1  33187  cycpmco2lem2  33188  cycpmco2lem3  33189  cycpmco2lem4  33190  cycpmco2lem5  33191  cycpmco2lem6  33192  cycpmco2lem7  33193  cycpmco2  33194  cycpm3cl2  33197  cycpmconjv  33203  tocyccntz  33205  cyc3evpm  33211  cycpmgcl  33214  cycpmconjslem2  33216  cyc3conja  33218  fxpval  33226  locfinreflem  33984  pstmval  34039  cntnevol  34372  omsval  34437  sitgval  34476  elprob  34553  cndprobval  34577  rrvmbfm  34586  bnj1385  34974  bnj1400  34977  bnj1014  35103  bnj1015  35104  bnj1326  35168  bnj1321  35169  bnj1491  35199  fineqvac  35260  mrsubfval  35690  rdgprc0  35973  dfrdg2  35975  brdomaing  36115  fwddifval  36344  fwddifnval  36345  filnetlem4  36563  cureq  37917  ismtyval  38121  isass  38167  isexid  38168  ismgmOLD  38171  elrefrels2  38919  elrefrels3  38920  refreleq  38922  elcnvrefrels2  38935  elcnvrefrels3  38936  elrefsymrels2  38974  eleqvrels2  38997  eleqvrels3  38998  dmqseq  39045  aomclem6  43487  aomclem8  43489  dfac21  43494  tfsconcatun  43765  tfsconcat0b  43774  tfsconcatrev  43776  rclexi  44042  rtrclex  44044  rtrclexi  44048  cnvrcl0  44052  dfrtrcl5  44056  dfrcl2  44101  gneispace2  44559  modelaxreplem1  45405  modelaxreplem2  45406  modelaxrep  45408  ssnnf1octb  45624  sge0val  46794  ismea  46879  caragenval  46921  isome  46922  issmflem  47155  isisubgr  48338  isgrim  48358  fnxpdmdm  48636  elbigo  49027  itcoval  49137  iinfprg  49534  infsubc2  49536  fucofvalne  49800