Theorem dmeq 5887

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ⊆ wss 3899  dom cdm 5655

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-dm 5665

This theorem is used by:  dmeqi  5888  dmeqd  5889  xpid11  5916  resresdm  6229  fneq1  6624  eqfnfv2  7024  funopdmsn  7148  nvof1o  7282  ofrfvalg  7687  offval  7688  offval3  7980  suppval  8161  smoeq  8340  tz7.44lem1  8395  tz7.44-2  8397  tz7.44-3  8398  ereq1  8707  cureq  8871  fundmeng  9042  fseqenlem2  10031  dfac3  10127  dfac9  10142  dfac12lem1  10149  dfac12r  10152  ackbij2lem2  10244  ackbij2lem3  10245  r1om  10248  cfsmolem  10275  cfsmo  10276  dcomex  10452  axdc2lem  10453  axdc3lem2  10456  axdc3lem4  10458  ac7g  10479  ttukey2g  10521  fundmge2nop0  14570  s4dom  14993  relexp0g  15098  relexpsucnnr  15101  dfrtrcl2  15138  ello1  15605  elo1  15616  bpolylem  16137  bpolyval  16138  isoval  17857  istsr  18674  ischn  18698  chnind  18712  islindf  22028  decpmatval0  22992  pmatcollpw3lem  23011  ordtval  23417  dfac14  23847  fmval  24172  fmf  24174  blfvalps  24612  tmsval  24710  cfilfval  25495  caufval  25506  isibl  25996  elcpn  26164  bdayval  27887  bdayfo  27916  nosupprefixmo  27939  noinfprefixmo  27940  nosupcbv  27941  nosupdm  27943  nosupfv  27945  nosupres  27946  nosupbnd1lem1  27947  nosupbnd1lem3  27949  nosupbnd1lem5  27951  nosupbnd2  27955  noinfcbv  27956  noinfdm  27958  noinffv  27960  noinfres  27961  noinfbnd1lem3  27964  noinfbnd1lem5  27966  noetasuplem4  27975  noetainflem4  27979  iscgrg  28857  uhgr0e  29531  incistruhgr  29539  ausgrusgri  29631  egrsubgr  29740  vtxdgfval  29930  vtxdg0e  29937  1egrvtxdg1  29972  eupth0  30697  ex-dm  30922  eldmne0  33103  of0r  33155  f1ocnt  33274  tocycfv  33552  tocycf  33560  tocyc01  33561  cycpmco2f1  33567  cycpmco2rn  33568  cycpmco2lem1  33569  cycpmco2lem2  33570  cycpmco2lem3  33571  cycpmco2lem4  33572  cycpmco2lem5  33573  cycpmco2lem6  33574  cycpmco2lem7  33575  cycpmco2  33576  cycpm3cl2  33579  cycpmconjv  33585  tocyccntz  33587  cyc3evpm  33593  cycpmgcl  33596  cycpmconjslem2  33598  cyc3conja  33600  fxpval  33608  locfinreflem  34353  pstmval  34408  cntnevol  34742  omsval  34807  sitgval  34846  elprob  34923  cndprobval  34947  rrvmbfm  34956  bnj1385  35344  bnj1400  35347  bnj1014  35473  bnj1015  35474  bnj1326  35538  bnj1321  35539  bnj1491  35569  fineqvac  35645  mrsubfval  36090  rdgprc0  36373  dfrdg2  36375  brdomaing  36515  fwddifval  36745  fwddifnval  36746  filnetlem4  37003  ismtyval  38553  isass  38599  isexid  38600  ismgmOLD  38603  elrefrels2  39349  elrefrels3  39350  refreleq  39352  elcnvrefrels2  39365  elcnvrefrels3  39366  elrefsymrels2  39404  eleqvrels2  39427  eleqvrels3  39428  dmqseq  39475  aomclem6  43903  aomclem8  43905  dfac21  43910  tfsconcatun  44181  tfsconcat0b  44190  tfsconcatrev  44192  rclexi  44458  rtrclex  44460  rtrclexi  44464  cnvrcl0  44468  dfrtrcl5  44472  dfrcl2  44517  gneispace2  44975  modelaxreplem1  45804  modelaxreplem2  45805  modelaxrep  45807  ssnnf1octb  46029  sge0val  47197  ismea  47282  caragenval  47324  isome  47325  issmflem  47558  isisubgr  48781  isgrim  48801  fnxpdmdm  49078  elbigo  49484  itcoval  49594  iinfprg  49988  infsubc2  49990  fucofvalne  50254