Theorem dmeq 5895

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 5894	. . 3 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)
2		dmss 5894	. . 3 ⊢ (𝐵 ⊆ 𝐴 → dom 𝐵 ⊆ dom 𝐴)
3	1, 2	anim12i 625	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (dom 𝐴 ⊆ dom 𝐵 ∧ dom 𝐵 ⊆ dom 𝐴))
4		eqss 3953	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
5		eqss 3953	. 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 3906  dom cdm 5663

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 2148  ax-9 2156  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-dm 5673

This theorem is used by:  dmeqi  5896  dmeqd  5897  xpid11  5924  resresdm  6236  fneq1  6630  eqfnfv2  7030  funopdmsn  7151  nvof1o  7284  ofrfvalg  7688  offval  7689  offval3  7981  suppval  8160  smoeq  8339  tz7.44lem1  8394  tz7.44-2  8396  tz7.44-3  8397  ereq1  8704  fundmeng  9032  fseqenlem2  10021  dfac3  10117  dfac9  10132  dfac12lem1  10139  dfac12r  10142  ackbij2lem2  10234  ackbij2lem3  10235  r1om  10238  cfsmolem  10265  cfsmo  10266  dcomex  10442  axdc2lem  10443  axdc3lem2  10446  axdc3lem4  10448  ac7g  10469  ttukey2g  10511  fundmge2nop0  14552  s4dom  14975  relexp0g  15078  relexpsucnnr  15081  dfrtrcl2  15118  ello1  15585  elo1  15596  bpolylem  16119  bpolyval  16120  isoval  17839  istsr  18656  ischn  18680  chnind  18694  islindf  21991  decpmatval0  22950  pmatcollpw3lem  22969  ordtval  23375  dfac14  23804  fmval  24129  fmf  24131  blfvalps  24569  tmsval  24667  cfilfval  25452  caufval  25463  isibl  25953  elcpn  26122  bdayval  27841  bdayfo  27870  nosupprefixmo  27893  noinfprefixmo  27894  nosupcbv  27895  nosupdm  27897  nosupfv  27899  nosupres  27900  nosupbnd1lem1  27901  nosupbnd1lem3  27903  nosupbnd1lem5  27905  nosupbnd2  27909  noinfcbv  27910  noinfdm  27912  noinffv  27914  noinfres  27915  noinfbnd1lem3  27918  noinfbnd1lem5  27920  noetasuplem4  27929  noetainflem4  27933  iscgrg  28810  uhgr0e  29450  incistruhgr  29458  ausgrusgri  29547  egrsubgr  29656  vtxdgfval  29846  vtxdg0e  29853  1egrvtxdg1  29888  eupth0  30594  ex-dm  30819  eldmne0  33001  of0r  33053  f1ocnt  33174  tocycfv  33452  tocycf  33460  tocyc01  33461  cycpmco2f1  33467  cycpmco2rn  33468  cycpmco2lem1  33469  cycpmco2lem2  33470  cycpmco2lem3  33471  cycpmco2lem4  33472  cycpmco2lem5  33473  cycpmco2lem6  33474  cycpmco2lem7  33475  cycpmco2  33476  cycpm3cl2  33479  cycpmconjv  33485  tocyccntz  33487  cyc3evpm  33493  cycpmgcl  33496  cycpmconjslem2  33498  cyc3conja  33500  fxpval  33508  locfinreflem  34253  pstmval  34308  cntnevol  34642  omsval  34707  sitgval  34746  elprob  34823  cndprobval  34847  rrvmbfm  34856  bnj1385  35244  bnj1400  35247  bnj1014  35373  bnj1015  35374  bnj1326  35438  bnj1321  35439  bnj1491  35469  fineqvac  35545  mrsubfval  36013  rdgprc0  36296  dfrdg2  36298  brdomaing  36438  fwddifval  36667  fwddifnval  36668  filnetlem4  36925  cureq  38280  ismtyval  38484  isass  38530  isexid  38531  ismgmOLD  38534  elrefrels2  39280  elrefrels3  39281  refreleq  39283  elcnvrefrels2  39296  elcnvrefrels3  39297  elrefsymrels2  39335  eleqvrels2  39358  eleqvrels3  39359  dmqseq  39406  aomclem6  43819  aomclem8  43821  dfac21  43826  tfsconcatun  44097  tfsconcat0b  44106  tfsconcatrev  44108  rclexi  44374  rtrclex  44376  rtrclexi  44380  cnvrcl0  44384  dfrtrcl5  44388  dfrcl2  44433  gneispace2  44891  modelaxreplem1  45720  modelaxreplem2  45721  modelaxrep  45723  ssnnf1octb  45945  sge0val  47113  ismea  47198  caragenval  47240  isome  47241  issmflem  47474  isisubgr  48660  isgrim  48680  fnxpdmdm  48958  elbigo  49364  itcoval  49474  iinfprg  49870  infsubc2  49872  fucofvalne  50136