Theorem dmeq 5246

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 5245	. . 3 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)
2		dmss 5245	. . 3 ⊢ (𝐵 ⊆ 𝐴 → dom 𝐵 ⊆ dom 𝐴)
3	1, 2	anim12i 588	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (dom 𝐴 ⊆ dom 𝐵 ∧ dom 𝐵 ⊆ dom 𝐴))
4		eqss 3583	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
5		eqss 3583	. 2 ⊢ (dom 𝐴 = dom 𝐵 ↔ (dom 𝐴 ⊆ dom 𝐵 ∧ dom 𝐵 ⊆ dom 𝐴))
6	3, 4, 5	3imtr4i 280	1 ⊢ (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475   ⊆ wss 3540  dom cdm 5038

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-dm 5048

This theorem is referenced by:  dmeqi  5247  dmeqd  5248  xpid11  5268  fneq1  5893  eqfnfv2  6220  nvof1o  6436  offval  6802  ofrfval  6803  offval3  7053  suppval  7184  smoeq  7334  tz7.44lem1  7388  tz7.44-2  7390  tz7.44-3  7391  ereq1  7636  fundmeng  7917  fseqenlem2  8731  dfac3  8827  dfac9  8841  dfac12lem1  8848  dfac12r  8851  ackbij2lem2  8945  ackbij2lem3  8946  r1om  8949  cfsmolem  8975  cfsmo  8976  dcomex  9152  axdc2lem  9153  axdc3lem2  9156  axdc3lem4  9158  ac7g  9179  ttukey2g  9221  fundmge2nop0  13129  s4dom  13514  relexp0g  13610  relexpsucnnr  13613  dfrtrcl2  13650  ello1  14094  elo1  14105  bpolylem  14618  bpolyval  14619  isoval  16248  istsr  17040  islindf  19970  decpmatval0  20388  pmatcollpw3lem  20407  ordtval  20803  dfac14  21231  fmval  21557  fmf  21559  blfvalps  21998  tmsval  22096  cfilfval  22870  caufval  22881  isibl  23338  elcpn  23503  iscgrg  25207  structvtxvallem  25697  uhgr0e  25737  incistruhgr  25746  isuhgra  25827  uhgrac  25834  uhgraeq12d  25836  isuslgra  25872  isusgra  25873  usgraeq12d  25891  wlks  26047  wlkcompim  26054  wlkelwrd  26058  ex-dm  26688  f1ocnt  28946  locfinreflem  29235  pstmval  29266  cntnevol  29618  omsval  29682  sitgval  29721  elprob  29798  cndprobval  29822  rrvmbfm  29831  bnj1385  30157  bnj1400  30160  bnj1014  30284  bnj1015  30285  bnj1326  30348  bnj1321  30349  bnj1491  30379  mrsubfval  30659  rdgprc0  30943  dfrdg2  30945  frrlem5e  31032  bdayval  31045  bdayfo  31074  nofulllem5  31105  brdomaing  31212  fwddifval  31439  fwddifnval  31440  filnetlem4  31546  cureq  32555  ismtyval  32769  isass  32815  isexid  32816  ismgmOLD  32819  aomclem6  36647  aomclem8  36649  dfac21  36654  rclexi  36941  rtrclex  36943  rtrclexi  36947  cnvrcl0  36951  dfrtrcl5  36955  dfrcl2  36985  gneispace2  37450  ssnnf1octb  38377  sge0val  39259  ismea  39344  caragenval  39383  isome  39384  issmflem  39613  resresdm  40319  ausgrusgri  40398  egrsubgr  40501  vtxdgfval  40683  vtxdg0e  40689  1egrvtxdg1  40725  eupth0  41382  fnxpdmdm  41558  offval0  42093  elbigo  42143