Theorem dmeq 5888

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ⊆ wss 3931  dom cdm 5659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125  df-dm 5669

This theorem is referenced by:  dmeqi  5889  dmeqd  5890  xpid11  5917  resresdm  6227  fneq1  6634  eqfnfv2  7027  funopdmsn  7145  nvof1o  7278  ofrfvalg  7684  offval  7685  offval3  7986  suppval  8166  smoeq  8369  tz7.44lem1  8424  tz7.44-2  8426  tz7.44-3  8427  ereq1  8731  fundmeng  9051  fseqenlem2  10044  dfac3  10140  dfac9  10156  dfac12lem1  10163  dfac12r  10166  ackbij2lem2  10258  ackbij2lem3  10259  r1om  10262  cfsmolem  10289  cfsmo  10290  dcomex  10466  axdc2lem  10467  axdc3lem2  10470  axdc3lem4  10472  ac7g  10493  ttukey2g  10535  fundmge2nop0  14525  s4dom  14943  relexp0g  15046  relexpsucnnr  15049  dfrtrcl2  15086  ello1  15536  elo1  15547  bpolylem  16069  bpolyval  16070  isoval  17783  istsr  18598  islindf  21777  decpmatval0  22707  pmatcollpw3lem  22726  ordtval  23132  dfac14  23561  fmval  23886  fmf  23888  blfvalps  24327  tmsval  24425  cfilfval  25221  caufval  25232  isibl  25723  elcpn  25893  bdayval  27617  bdayfo  27646  nosupprefixmo  27669  noinfprefixmo  27670  nosupcbv  27671  nosupdm  27673  nosupfv  27675  nosupres  27676  nosupbnd1lem1  27677  nosupbnd1lem3  27679  nosupbnd1lem5  27681  nosupbnd2  27685  noinfcbv  27686  noinfdm  27688  noinffv  27690  noinfres  27691  noinfbnd1lem3  27694  noinfbnd1lem5  27696  noetasuplem4  27705  noetainflem4  27709  iscgrg  28496  uhgr0e  29055  incistruhgr  29063  ausgrusgri  29152  egrsubgr  29261  vtxdgfval  29452  vtxdg0e  29459  1egrvtxdg1  29494  eupth0  30200  ex-dm  30425  eldmne0  32611  of0r  32661  f1ocnt  32784  ischn  32991  chnind  32996  tocycfv  33125  tocycf  33133  tocyc01  33134  cycpmco2f1  33140  cycpmco2rn  33141  cycpmco2lem1  33142  cycpmco2lem2  33143  cycpmco2lem3  33144  cycpmco2lem4  33145  cycpmco2lem5  33146  cycpmco2lem6  33147  cycpmco2lem7  33148  cycpmco2  33149  cycpm3cl2  33152  cycpmconjv  33158  tocyccntz  33160  cyc3evpm  33166  cycpmgcl  33169  cycpmconjslem2  33171  cyc3conja  33173  locfinreflem  33876  pstmval  33931  cntnevol  34264  omsval  34330  sitgval  34369  elprob  34446  cndprobval  34470  rrvmbfm  34479  bnj1385  34868  bnj1400  34871  bnj1014  34997  bnj1015  34998  bnj1326  35062  bnj1321  35063  bnj1491  35093  fineqvac  35133  mrsubfval  35535  rdgprc0  35816  dfrdg2  35818  brdomaing  35958  fwddifval  36185  fwddifnval  36186  filnetlem4  36404  cureq  37625  ismtyval  37829  isass  37875  isexid  37876  ismgmOLD  37879  elrefrels2  38541  elrefrels3  38542  refreleq  38544  elcnvrefrels2  38557  elcnvrefrels3  38558  elrefsymrels2  38592  eleqvrels2  38615  eleqvrels3  38616  dmqseq  38663  aomclem6  43058  aomclem8  43060  dfac21  43065  tfsconcatun  43336  tfsconcat0b  43345  tfsconcatrev  43347  rclexi  43614  rtrclex  43616  rtrclexi  43620  cnvrcl0  43624  dfrtrcl5  43628  dfrcl2  43673  gneispace2  44131  modelaxreplem1  44978  modelaxreplem2  44979  modelaxrep  44981  ssnnf1octb  45198  sge0val  46375  ismea  46460  caragenval  46502  isome  46503  issmflem  46736  isisubgr  47855  isgrim  47875  fnxpdmdm  48115  elbigo  48511  itcoval  48621  iinfprg  49006  infsubc2  49008  fucofvalne  49216