Theorem dmeq 5843

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 5842	. . 3 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)
2		dmss 5842	. . 3 ⊢ (𝐵 ⊆ 𝐴 → dom 𝐵 ⊆ dom 𝐴)
3	1, 2	anim12i 613	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (dom 𝐴 ⊆ dom 𝐵 ∧ dom 𝐵 ⊆ dom 𝐴))
4		eqss 3950	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
5		eqss 3950	. 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 3902  dom cdm 5616

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-br 5092  df-dm 5626

This theorem is referenced by:  dmeqi  5844  dmeqd  5845  xpid11  5872  resresdm  6180  fneq1  6572  eqfnfv2  6965  funopdmsn  7083  nvof1o  7214  ofrfvalg  7618  offval  7619  offval3  7914  suppval  8092  smoeq  8270  tz7.44lem1  8324  tz7.44-2  8326  tz7.44-3  8327  ereq1  8629  fundmeng  8954  fseqenlem2  9916  dfac3  10012  dfac9  10028  dfac12lem1  10035  dfac12r  10038  ackbij2lem2  10130  ackbij2lem3  10131  r1om  10134  cfsmolem  10161  cfsmo  10162  dcomex  10338  axdc2lem  10339  axdc3lem2  10342  axdc3lem4  10344  ac7g  10365  ttukey2g  10407  fundmge2nop0  14409  s4dom  14826  relexp0g  14929  relexpsucnnr  14932  dfrtrcl2  14969  ello1  15422  elo1  15433  bpolylem  15955  bpolyval  15956  isoval  17672  istsr  18489  ischn  18513  chnind  18527  islindf  21750  decpmatval0  22680  pmatcollpw3lem  22699  ordtval  23105  dfac14  23534  fmval  23859  fmf  23861  blfvalps  24299  tmsval  24397  cfilfval  25192  caufval  25203  isibl  25694  elcpn  25864  bdayval  27588  bdayfo  27617  nosupprefixmo  27640  noinfprefixmo  27641  nosupcbv  27642  nosupdm  27644  nosupfv  27646  nosupres  27647  nosupbnd1lem1  27648  nosupbnd1lem3  27650  nosupbnd1lem5  27652  nosupbnd2  27656  noinfcbv  27657  noinfdm  27659  noinffv  27661  noinfres  27662  noinfbnd1lem3  27665  noinfbnd1lem5  27667  noetasuplem4  27676  noetainflem4  27680  iscgrg  28491  uhgr0e  29050  incistruhgr  29058  ausgrusgri  29147  egrsubgr  29256  vtxdgfval  29447  vtxdg0e  29454  1egrvtxdg1  29489  eupth0  30192  ex-dm  30417  eldmne0  32607  of0r  32658  f1ocnt  32780  tocycfv  33076  tocycf  33084  tocyc01  33085  cycpmco2f1  33091  cycpmco2rn  33092  cycpmco2lem1  33093  cycpmco2lem2  33094  cycpmco2lem3  33095  cycpmco2lem4  33096  cycpmco2lem5  33097  cycpmco2lem6  33098  cycpmco2lem7  33099  cycpmco2  33100  cycpm3cl2  33103  cycpmconjv  33109  tocyccntz  33111  cyc3evpm  33117  cycpmgcl  33120  cycpmconjslem2  33122  cyc3conja  33124  fxpval  33132  locfinreflem  33851  pstmval  33906  cntnevol  34239  omsval  34304  sitgval  34343  elprob  34420  cndprobval  34444  rrvmbfm  34453  bnj1385  34842  bnj1400  34845  bnj1014  34971  bnj1015  34972  bnj1326  35036  bnj1321  35037  bnj1491  35067  fineqvac  35137  mrsubfval  35550  rdgprc0  35833  dfrdg2  35835  brdomaing  35975  fwddifval  36202  fwddifnval  36203  filnetlem4  36421  cureq  37642  ismtyval  37846  isass  37892  isexid  37893  ismgmOLD  37896  elrefrels2  38561  elrefrels3  38562  refreleq  38564  elcnvrefrels2  38577  elcnvrefrels3  38578  elrefsymrels2  38612  eleqvrels2  38635  eleqvrels3  38636  dmqseq  38683  aomclem6  43098  aomclem8  43100  dfac21  43105  tfsconcatun  43376  tfsconcat0b  43385  tfsconcatrev  43387  rclexi  43654  rtrclex  43656  rtrclexi  43660  cnvrcl0  43664  dfrtrcl5  43668  dfrcl2  43713  gneispace2  44171  modelaxreplem1  45017  modelaxreplem2  45018  modelaxrep  45020  ssnnf1octb  45237  sge0val  46410  ismea  46495  caragenval  46537  isome  46538  issmflem  46771  isisubgr  47899  isgrim  47919  fnxpdmdm  48197  elbigo  48589  itcoval  48699  iinfprg  49097  infsubc2  49099  fucofvalne  49363