Theorem dmeq 5766

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 5765	. . 3 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)
2		dmss 5765	. . 3 ⊢ (𝐵 ⊆ 𝐴 → dom 𝐵 ⊆ dom 𝐴)
3	1, 2	anim12i 614	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (dom 𝐴 ⊆ dom 𝐵 ∧ dom 𝐵 ⊆ dom 𝐴))
4		eqss 3981	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
5		eqss 3981	. 2 ⊢ (dom 𝐴 = dom 𝐵 ↔ (dom 𝐴 ⊆ dom 𝐵 ∧ dom 𝐵 ⊆ dom 𝐴))
6	3, 4, 5	3imtr4i 294	1 ⊢ (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1533   ⊆ wss 3935  dom cdm 5549

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4561  df-pr 4563  df-op 4567  df-br 5059  df-dm 5559

This theorem is referenced by:  dmeqi  5767  dmeqd  5768  xpid11  5796  resresdm  6084  fneq1  6438  eqfnfv2  6797  funopdmsn  6906  nvof1o  7031  offval  7410  ofrfval  7411  offval3  7677  suppval  7826  smoeq  7981  tz7.44lem1  8035  tz7.44-2  8037  tz7.44-3  8038  ereq1  8290  fundmeng  8578  fseqenlem2  9445  dfac3  9541  dfac9  9556  dfac12lem1  9563  dfac12r  9566  ackbij2lem2  9656  ackbij2lem3  9657  r1om  9660  cfsmolem  9686  cfsmo  9687  dcomex  9863  axdc2lem  9864  axdc3lem2  9867  axdc3lem4  9869  ac7g  9890  ttukey2g  9932  fundmge2nop0  13844  s4dom  14275  relexp0g  14375  relexpsucnnr  14378  dfrtrcl2  14415  ello1  14866  elo1  14877  bpolylem  15396  bpolyval  15397  isoval  17029  istsr  17821  islindf  20950  decpmatval0  21366  pmatcollpw3lem  21385  ordtval  21791  dfac14  22220  fmval  22545  fmf  22547  blfvalps  22987  tmsval  23085  cfilfval  23861  caufval  23872  isibl  24360  elcpn  24525  iscgrg  26292  uhgr0e  26850  incistruhgr  26858  ausgrusgri  26947  egrsubgr  27053  vtxdgfval  27243  vtxdg0e  27250  1egrvtxdg1  27285  eupth0  27987  ex-dm  28212  eldmne0  30367  f1ocnt  30519  tocycfv  30746  tocycf  30754  tocyc01  30755  cycpmco2f1  30761  cycpmco2rn  30762  cycpmco2lem1  30763  cycpmco2lem2  30764  cycpmco2lem3  30765  cycpmco2lem4  30766  cycpmco2lem5  30767  cycpmco2lem6  30768  cycpmco2lem7  30769  cycpmco2  30770  cycpm3cl2  30773  cycpmconjv  30779  tocyccntz  30781  cyc3evpm  30787  cycpmgcl  30790  cycpmconjslem2  30792  cyc3conja  30794  locfinreflem  31099  pstmval  31130  cntnevol  31482  omsval  31546  sitgval  31585  elprob  31662  cndprobval  31686  rrvmbfm  31695  bnj1385  32099  bnj1400  32102  bnj1014  32228  bnj1015  32229  bnj1326  32293  bnj1321  32294  bnj1491  32324  mrsubfval  32750  rdgprc0  33033  dfrdg2  33035  bdayval  33150  bdayfo  33177  noprefixmo  33197  nosupdm  33199  nosupfv  33201  nosupres  33202  nosupbnd1lem1  33203  nosupbnd1lem3  33205  nosupbnd1lem5  33207  nosupbnd2  33211  noetalem3  33214  brdomaing  33391  fwddifval  33618  fwddifnval  33619  filnetlem4  33724  cureq  34862  ismtyval  35072  isass  35118  isexid  35119  ismgmOLD  35122  elrefrels2  35751  elrefrels3  35752  refreleq  35754  elcnvrefrels2  35764  elcnvrefrels3  35765  elrefsymrels2  35799  eleqvrels2  35821  eleqvrels3  35822  dmqseq  35869  aomclem6  39652  aomclem8  39654  dfac21  39659  rclexi  39968  rtrclex  39970  rtrclexi  39974  cnvrcl0  39978  dfrtrcl5  39982  dfrcl2  40012  gneispace2  40475  ssnnf1octb  41449  sge0val  42642  ismea  42727  caragenval  42769  isome  42770  issmflem  42998  isomgreqve  43984  fnxpdmdm  44029  elbigo  44605