Theorem dmeq 5849

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5096  df-dm 5631

This theorem is referenced by:  dmeqi  5850  dmeqd  5851  xpid11  5878  resresdm  6187  fneq1  6579  eqfnfv2  6973  funopdmsn  7091  nvof1o  7222  ofrfvalg  7626  offval  7627  offval3  7922  suppval  8100  smoeq  8278  tz7.44lem1  8332  tz7.44-2  8334  tz7.44-3  8335  ereq1  8637  fundmeng  8963  fseqenlem2  9925  dfac3  10021  dfac9  10037  dfac12lem1  10044  dfac12r  10047  ackbij2lem2  10139  ackbij2lem3  10140  r1om  10143  cfsmolem  10170  cfsmo  10171  dcomex  10347  axdc2lem  10348  axdc3lem2  10351  axdc3lem4  10353  ac7g  10374  ttukey2g  10416  fundmge2nop0  14413  s4dom  14830  relexp0g  14933  relexpsucnnr  14936  dfrtrcl2  14973  ello1  15426  elo1  15437  bpolylem  15959  bpolyval  15960  isoval  17676  istsr  18493  ischn  18517  chnind  18531  islindf  21753  decpmatval0  22682  pmatcollpw3lem  22701  ordtval  23107  dfac14  23536  fmval  23861  fmf  23863  blfvalps  24301  tmsval  24399  cfilfval  25194  caufval  25205  isibl  25696  elcpn  25866  bdayval  27590  bdayfo  27619  nosupprefixmo  27642  noinfprefixmo  27643  nosupcbv  27644  nosupdm  27646  nosupfv  27648  nosupres  27649  nosupbnd1lem1  27650  nosupbnd1lem3  27652  nosupbnd1lem5  27654  nosupbnd2  27658  noinfcbv  27659  noinfdm  27661  noinffv  27663  noinfres  27664  noinfbnd1lem3  27667  noinfbnd1lem5  27669  noetasuplem4  27678  noetainflem4  27682  iscgrg  28493  uhgr0e  29053  incistruhgr  29061  ausgrusgri  29150  egrsubgr  29259  vtxdgfval  29450  vtxdg0e  29457  1egrvtxdg1  29492  eupth0  30198  ex-dm  30423  eldmne0  32613  of0r  32666  f1ocnt  32789  tocycfv  33087  tocycf  33095  tocyc01  33096  cycpmco2f1  33102  cycpmco2rn  33103  cycpmco2lem1  33104  cycpmco2lem2  33105  cycpmco2lem3  33106  cycpmco2lem4  33107  cycpmco2lem5  33108  cycpmco2lem6  33109  cycpmco2lem7  33110  cycpmco2  33111  cycpm3cl2  33114  cycpmconjv  33120  tocyccntz  33122  cyc3evpm  33128  cycpmgcl  33131  cycpmconjslem2  33133  cyc3conja  33135  fxpval  33143  locfinreflem  33876  pstmval  33931  cntnevol  34264  omsval  34329  sitgval  34368  elprob  34445  cndprobval  34469  rrvmbfm  34478  bnj1385  34867  bnj1400  34870  bnj1014  34996  bnj1015  34997  bnj1326  35061  bnj1321  35062  bnj1491  35092  fineqvac  35162  mrsubfval  35575  rdgprc0  35858  dfrdg2  35860  brdomaing  36000  fwddifval  36229  fwddifnval  36230  filnetlem4  36448  cureq  37659  ismtyval  37863  isass  37909  isexid  37910  ismgmOLD  37913  elrefrels2  38633  elrefrels3  38634  refreleq  38636  elcnvrefrels2  38649  elcnvrefrels3  38650  elrefsymrels2  38688  eleqvrels2  38711  eleqvrels3  38712  dmqseq  38760  aomclem6  43179  aomclem8  43181  dfac21  43186  tfsconcatun  43457  tfsconcat0b  43466  tfsconcatrev  43468  rclexi  43735  rtrclex  43737  rtrclexi  43741  cnvrcl0  43745  dfrtrcl5  43749  dfrcl2  43794  gneispace2  44252  modelaxreplem1  45098  modelaxreplem2  45099  modelaxrep  45101  ssnnf1octb  45318  sge0val  46491  ismea  46576  caragenval  46618  isome  46619  issmflem  46852  isisubgr  47989  isgrim  48009  fnxpdmdm  48287  elbigo  48679  itcoval  48789  iinfprg  49187  infsubc2  49189  fucofvalne  49453