Theorem dmeq 5885

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 5884	. . 3 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)
2		dmss 5884	. . 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 5651

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 2733

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 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  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 5661

This theorem is used by:  dmeqi  5886  dmeqd  5887  xpid11  5914  resresdm  6233  fneq1  6628  eqfnfv2  7028  funopdmsn  7152  nvof1o  7286  ofrfvalg  7699  offval  7700  offval3  7992  suppval  8172  smoeq  8351  tz7.44lem1  8406  tz7.44-2  8408  tz7.44-3  8409  ereq1  8718  cureq  8882  fundmeng  9053  fseqenlem2  10097  dfac3  10193  dfac9  10208  dfac12lem1  10215  dfac12r  10218  ackbij2lem2  10310  ackbij2lem3  10311  hfom  10314  cfsmolem  10341  cfsmo  10342  dcomex  10518  axdc2lem  10519  axdc3lem2  10522  axdc3lem4  10524  ac7g  10545  ttukey2g  10587  fundmge2nop0  14640  s4dom  15063  relexp0g  15168  relexpsucnnr  15171  dfrtrcl2  15208  ello1  15675  elo1  15686  bpolylem  16207  bpolyval  16208  isoval  17933  istsr  18750  ischn  18774  chnind  18788  islindf  22111  decpmatval0  23075  pmatcollpw3lem  23094  ordtval  23500  dfac14  23930  fmval  24255  fmf  24257  blfvalps  24695  tmsval  24793  cfilfval  25578  caufval  25589  isibl  26079  elcpn  26247  bdayval  27998  bdayfo  28027  nosupprefixmo  28050  noinfprefixmo  28051  nosupcbv  28052  nosupdm  28054  nosupfv  28056  nosupres  28057  nosupbnd1lem1  28058  nosupbnd1lem3  28060  nosupbnd1lem5  28062  nosupbnd2  28066  noinfcbv  28067  noinfdm  28069  noinffv  28071  noinfres  28072  noinfbnd1lem3  28075  noinfbnd1lem5  28077  noetasuplem4  28086  noetainflem4  28090  iscgrg  28968  uhgr0e  29642  incistruhgr  29650  ausgrusgri  29742  egrsubgr  29851  vtxdgfval  30041  vtxdg0e  30048  1egrvtxdg1  30083  eupth0  30808  ex-dm  31033  eldmne0  33214  of0r  33266  f1ocnt  33385  tocycfv  33663  tocycf  33671  tocyc01  33672  cycpmco2f1  33678  cycpmco2rn  33679  cycpmco2lem1  33680  cycpmco2lem2  33681  cycpmco2lem3  33682  cycpmco2lem4  33683  cycpmco2lem5  33684  cycpmco2lem6  33685  cycpmco2lem7  33686  cycpmco2  33687  cycpm3cl2  33690  cycpmconjv  33696  tocyccntz  33698  cyc3evpm  33704  cycpmgcl  33707  cycpmconjslem2  33709  cyc3conja  33711  fxpval  33719  locfinreflem  34465  pstmval  34520  cntnevol  34854  omsval  34918  sitgval  34957  elprob  35034  cndprobval  35058  rrvmbfm  35067  bnj1385  35455  bnj1400  35458  bnj1014  35584  bnj1015  35585  bnj1326  35649  bnj1321  35650  bnj1491  35680  fineqvac  35767  mrsubfval  36252  rdgprc0  36535  dfrdg2  36537  brdomaing  36677  fwddifval  36907  fwddifnval  36908  filnetlem4  37149  ismtyval  38714  isass  38760  isexid  38761  ismgmOLD  38764  elrefrels2  39510  elrefrels3  39511  refreleq  39513  elcnvrefrels2  39526  elcnvrefrels3  39527  elrefsymrels2  39565  eleqvrels2  39588  eleqvrels3  39589  dmqseq  39636  aomclem6  44045  aomclem8  44047  dfac21  44052  tfsconcatun  44323  tfsconcat0b  44332  tfsconcatrev  44334  rclexi  44600  rtrclex  44602  rtrclexi  44606  cnvrcl0  44610  dfrtrcl5  44614  dfrcl2  44659  gneispace2  45117  modelaxreplem1  45946  modelaxreplem2  45947  modelaxrep  45949  ssnnf1octb  46178  sge0val  47345  ismea  47430  caragenval  47472  isome  47473  issmflem  47706  isisubgr  48929  isgrim  48949  fnxpdmdm  49226  elbigo  49632  itcoval  49742  iinfprg  50136  infsubc2  50138  fucofvalne  50402