Theorem dmeq 5860

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 5859	. . 3 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)
2		dmss 5859	. . 3 ⊢ (𝐵 ⊆ 𝐴 → dom 𝐵 ⊆ dom 𝐴)
3	1, 2	anim12i 614	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (dom 𝐴 ⊆ dom 𝐵 ∧ dom 𝐵 ⊆ dom 𝐴))
4		eqss 3951	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
5		eqss 3951	. 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 3903  dom cdm 5632

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-dm 5642

This theorem is referenced by:  dmeqi  5861  dmeqd  5862  xpid11  5889  resresdm  6199  fneq1  6591  eqfnfv2  6986  funopdmsn  7105  nvof1o  7236  ofrfvalg  7640  offval  7641  offval3  7936  suppval  8114  smoeq  8292  tz7.44lem1  8346  tz7.44-2  8348  tz7.44-3  8349  ereq1  8653  fundmeng  8981  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  14437  s4dom  14854  relexp0g  14957  relexpsucnnr  14960  dfrtrcl2  14997  ello1  15450  elo1  15461  bpolylem  15983  bpolyval  15984  isoval  17701  istsr  18518  ischn  18542  chnind  18556  islindf  21779  decpmatval0  22720  pmatcollpw3lem  22739  ordtval  23145  dfac14  23574  fmval  23899  fmf  23901  blfvalps  24339  tmsval  24437  cfilfval  25232  caufval  25243  isibl  25734  elcpn  25904  bdayval  27628  bdayfo  27657  nosupprefixmo  27680  noinfprefixmo  27681  nosupcbv  27682  nosupdm  27684  nosupfv  27686  nosupres  27687  nosupbnd1lem1  27688  nosupbnd1lem3  27690  nosupbnd1lem5  27692  nosupbnd2  27696  noinfcbv  27697  noinfdm  27699  noinffv  27701  noinfres  27702  noinfbnd1lem3  27705  noinfbnd1lem5  27707  noetasuplem4  27716  noetainflem4  27720  iscgrg  28596  uhgr0e  29156  incistruhgr  29164  ausgrusgri  29253  egrsubgr  29362  vtxdgfval  29553  vtxdg0e  29560  1egrvtxdg1  29595  eupth0  30301  ex-dm  30526  eldmne0  32716  of0r  32768  f1ocnt  32890  tocycfv  33202  tocycf  33210  tocyc01  33211  cycpmco2f1  33217  cycpmco2rn  33218  cycpmco2lem1  33219  cycpmco2lem2  33220  cycpmco2lem3  33221  cycpmco2lem4  33222  cycpmco2lem5  33223  cycpmco2lem6  33224  cycpmco2lem7  33225  cycpmco2  33226  cycpm3cl2  33229  cycpmconjv  33235  tocyccntz  33237  cyc3evpm  33243  cycpmgcl  33246  cycpmconjslem2  33248  cyc3conja  33250  fxpval  33258  locfinreflem  34017  pstmval  34072  cntnevol  34405  omsval  34470  sitgval  34509  elprob  34586  cndprobval  34610  rrvmbfm  34619  bnj1385  35007  bnj1400  35010  bnj1014  35136  bnj1015  35137  bnj1326  35201  bnj1321  35202  bnj1491  35232  fineqvac  35291  mrsubfval  35721  rdgprc0  36004  dfrdg2  36006  brdomaing  36146  fwddifval  36375  fwddifnval  36376  filnetlem4  36594  cureq  37844  ismtyval  38048  isass  38094  isexid  38095  ismgmOLD  38098  elrefrels2  38846  elrefrels3  38847  refreleq  38849  elcnvrefrels2  38862  elcnvrefrels3  38863  elrefsymrels2  38901  eleqvrels2  38924  eleqvrels3  38925  dmqseq  38972  aomclem6  43413  aomclem8  43415  dfac21  43420  tfsconcatun  43691  tfsconcat0b  43700  tfsconcatrev  43702  rclexi  43968  rtrclex  43970  rtrclexi  43974  cnvrcl0  43978  dfrtrcl5  43982  dfrcl2  44027  gneispace2  44485  modelaxreplem1  45331  modelaxreplem2  45332  modelaxrep  45334  ssnnf1octb  45550  sge0val  46721  ismea  46806  caragenval  46848  isome  46849  issmflem  47082  isisubgr  48219  isgrim  48239  fnxpdmdm  48517  elbigo  48908  itcoval  49018  iinfprg  49415  infsubc2  49417  fucofvalne  49681