Theorem dmeq 5895

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ⊆ wss 3906  dom cdm 5663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-dm 5673

This theorem is referenced by:  dmeqi  5896  dmeqd  5897  xpid11  5924  resresdm  6236  fneq1  6628  eqfnfv2  7028  funopdmsn  7149  nvof1o  7280  ofrfvalg  7684  offval  7685  offval3  7980  suppval  8159  smoeq  8338  tz7.44lem1  8393  tz7.44-2  8395  tz7.44-3  8396  ereq1  8703  fundmeng  9030  fseqenlem2  10010  dfac3  10106  dfac9  10121  dfac12lem1  10128  dfac12r  10131  ackbij2lem2  10223  ackbij2lem3  10224  r1om  10227  cfsmolem  10255  cfsmo  10256  dcomex  10432  axdc2lem  10433  axdc3lem2  10436  axdc3lem4  10438  ac7g  10459  ttukey2g  10501  fundmge2nop0  14541  s4dom  14958  relexp0g  15061  relexpsucnnr  15064  dfrtrcl2  15101  ello1  15568  elo1  15579  bpolylem  16103  bpolyval  16104  isoval  17823  istsr  18640  ischn  18664  chnind  18678  islindf  21943  decpmatval0  22902  pmatcollpw3lem  22921  ordtval  23327  dfac14  23756  fmval  24081  fmf  24083  blfvalps  24521  tmsval  24619  cfilfval  25404  caufval  25415  isibl  25905  elcpn  26074  bdayval  27793  bdayfo  27822  nosupprefixmo  27845  noinfprefixmo  27846  nosupcbv  27847  nosupdm  27849  nosupfv  27851  nosupres  27852  nosupbnd1lem1  27853  nosupbnd1lem3  27855  nosupbnd1lem5  27857  nosupbnd2  27861  noinfcbv  27862  noinfdm  27864  noinffv  27866  noinfres  27867  noinfbnd1lem3  27870  noinfbnd1lem5  27872  noetasuplem4  27881  noetainflem4  27885  iscgrg  28762  uhgr0e  29402  incistruhgr  29410  ausgrusgri  29499  egrsubgr  29608  vtxdgfval  29798  vtxdg0e  29805  1egrvtxdg1  29840  eupth0  30546  ex-dm  30771  eldmne0  32953  of0r  33005  f1ocnt  33126  tocycfv  33410  tocycf  33418  tocyc01  33419  cycpmco2f1  33425  cycpmco2rn  33426  cycpmco2lem1  33427  cycpmco2lem2  33428  cycpmco2lem3  33429  cycpmco2lem4  33430  cycpmco2lem5  33431  cycpmco2lem6  33432  cycpmco2lem7  33433  cycpmco2  33434  cycpm3cl2  33437  cycpmconjv  33443  tocyccntz  33445  cyc3evpm  33451  cycpmgcl  33454  cycpmconjslem2  33456  cyc3conja  33458  fxpval  33466  locfinreflem  34211  pstmval  34266  cntnevol  34599  omsval  34664  sitgval  34703  elprob  34780  cndprobval  34804  rrvmbfm  34813  bnj1385  35201  bnj1400  35204  bnj1014  35330  bnj1015  35331  bnj1326  35395  bnj1321  35396  bnj1491  35426  fineqvac  35510  mrsubfval  35981  rdgprc0  36264  dfrdg2  36266  brdomaing  36406  fwddifval  36635  fwddifnval  36636  filnetlem4  36873  cureq  38228  ismtyval  38432  isass  38478  isexid  38479  ismgmOLD  38482  elrefrels2  39228  elrefrels3  39229  refreleq  39231  elcnvrefrels2  39244  elcnvrefrels3  39245  elrefsymrels2  39283  eleqvrels2  39306  eleqvrels3  39307  dmqseq  39354  aomclem6  43769  aomclem8  43771  dfac21  43776  tfsconcatun  44047  tfsconcat0b  44056  tfsconcatrev  44058  rclexi  44324  rtrclex  44326  rtrclexi  44330  cnvrcl0  44334  dfrtrcl5  44338  dfrcl2  44383  gneispace2  44841  modelaxreplem1  45670  modelaxreplem2  45671  modelaxrep  45673  ssnnf1octb  45895  sge0val  47063  ismea  47148  caragenval  47190  isome  47191  issmflem  47424  isisubgr  48610  isgrim  48630  fnxpdmdm  48908  elbigo  49314  itcoval  49424  iinfprg  49820  infsubc2  49822  fucofvalne  50086