Theorem dmeq 5913

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ⊆ wss 3950  dom cdm 5684

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-br 5143  df-dm 5694

This theorem is referenced by:  dmeqi  5914  dmeqd  5915  xpid11  5942  resresdm  6252  fneq1  6658  eqfnfv2  7051  funopdmsn  7169  nvof1o  7301  ofrfvalg  7706  offval  7707  offval3  8008  suppval  8188  smoeq  8391  tz7.44lem1  8446  tz7.44-2  8448  tz7.44-3  8449  ereq1  8753  fundmeng  9073  fseqenlem2  10066  dfac3  10162  dfac9  10178  dfac12lem1  10185  dfac12r  10188  ackbij2lem2  10280  ackbij2lem3  10281  r1om  10284  cfsmolem  10311  cfsmo  10312  dcomex  10488  axdc2lem  10489  axdc3lem2  10492  axdc3lem4  10494  ac7g  10515  ttukey2g  10557  fundmge2nop0  14542  s4dom  14959  relexp0g  15062  relexpsucnnr  15065  dfrtrcl2  15102  ello1  15552  elo1  15563  bpolylem  16085  bpolyval  16086  isoval  17810  istsr  18629  islindf  21833  decpmatval0  22771  pmatcollpw3lem  22790  ordtval  23198  dfac14  23627  fmval  23952  fmf  23954  blfvalps  24394  tmsval  24494  cfilfval  25299  caufval  25310  isibl  25801  elcpn  25971  bdayval  27694  bdayfo  27723  nosupprefixmo  27746  noinfprefixmo  27747  nosupcbv  27748  nosupdm  27750  nosupfv  27752  nosupres  27753  nosupbnd1lem1  27754  nosupbnd1lem3  27756  nosupbnd1lem5  27758  nosupbnd2  27762  noinfcbv  27763  noinfdm  27765  noinffv  27767  noinfres  27768  noinfbnd1lem3  27771  noinfbnd1lem5  27773  noetasuplem4  27782  noetainflem4  27786  iscgrg  28521  uhgr0e  29089  incistruhgr  29097  ausgrusgri  29186  egrsubgr  29295  vtxdgfval  29486  vtxdg0e  29493  1egrvtxdg1  29528  eupth0  30234  ex-dm  30459  eldmne0  32639  of0r  32689  f1ocnt  32805  ischn  32997  chnind  33002  tocycfv  33130  tocycf  33138  tocyc01  33139  cycpmco2f1  33145  cycpmco2rn  33146  cycpmco2lem1  33147  cycpmco2lem2  33148  cycpmco2lem3  33149  cycpmco2lem4  33150  cycpmco2lem5  33151  cycpmco2lem6  33152  cycpmco2lem7  33153  cycpmco2  33154  cycpm3cl2  33157  cycpmconjv  33163  tocyccntz  33165  cyc3evpm  33171  cycpmgcl  33174  cycpmconjslem2  33176  cyc3conja  33178  locfinreflem  33840  pstmval  33895  cntnevol  34230  omsval  34296  sitgval  34335  elprob  34412  cndprobval  34436  rrvmbfm  34445  bnj1385  34847  bnj1400  34850  bnj1014  34976  bnj1015  34977  bnj1326  35041  bnj1321  35042  bnj1491  35072  fineqvac  35112  mrsubfval  35514  rdgprc0  35795  dfrdg2  35797  brdomaing  35937  fwddifval  36164  fwddifnval  36165  filnetlem4  36383  cureq  37604  ismtyval  37808  isass  37854  isexid  37855  ismgmOLD  37858  elrefrels2  38520  elrefrels3  38521  refreleq  38523  elcnvrefrels2  38536  elcnvrefrels3  38537  elrefsymrels2  38571  eleqvrels2  38594  eleqvrels3  38595  dmqseq  38642  aomclem6  43076  aomclem8  43078  dfac21  43083  tfsconcatun  43355  tfsconcat0b  43364  tfsconcatrev  43366  rclexi  43633  rtrclex  43635  rtrclexi  43639  cnvrcl0  43643  dfrtrcl5  43647  dfrcl2  43692  gneispace2  44150  modelaxreplem1  45000  modelaxreplem2  45001  modelaxrep  45003  ssnnf1octb  45204  sge0val  46386  ismea  46471  caragenval  46513  isome  46514  issmflem  46747  isisubgr  47853  isgrim  47873  fnxpdmdm  48081  elbigo  48477  itcoval  48587  fucofvalne  49043