Theorem dmeq 5615

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 5614	. . 3 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)
2		dmss 5614	. . 3 ⊢ (𝐵 ⊆ 𝐴 → dom 𝐵 ⊆ dom 𝐴)
3	1, 2	anim12i 603	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (dom 𝐴 ⊆ dom 𝐵 ∧ dom 𝐵 ⊆ dom 𝐴))
4		eqss 3869	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
5		eqss 3869	. 2 ⊢ (dom 𝐴 = dom 𝐵 ↔ (dom 𝐴 ⊆ dom 𝐵 ∧ dom 𝐵 ⊆ dom 𝐴))
6	3, 4, 5	3imtr4i 284	1 ⊢ (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)

Syntax hints:   → wi 4   ∧ wa 387   = wceq 1507   ⊆ wss 3825  dom cdm 5400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-rab 3091  df-v 3411  df-dif 3828  df-un 3830  df-in 3832  df-ss 3839  df-nul 4174  df-if 4345  df-sn 4436  df-pr 4438  df-op 4442  df-br 4924  df-dm 5410

This theorem is referenced by:  dmeqi  5616  dmeqd  5617  xpid11  5638  resresdm  5923  fneq1  6271  eqfnfv2  6622  funopdmsn  6729  nvof1o  6856  offval  7228  ofrfval  7229  offval3  7488  suppval  7628  smoeq  7784  tz7.44lem1  7838  tz7.44-2  7840  tz7.44-3  7841  ereq1  8088  fundmeng  8373  fseqenlem2  9237  dfac3  9333  dfac9  9348  dfac12lem1  9355  dfac12r  9358  ackbij2lem2  9452  ackbij2lem3  9453  r1om  9456  cfsmolem  9482  cfsmo  9483  dcomex  9659  axdc2lem  9660  axdc3lem2  9663  axdc3lem4  9665  ac7g  9686  ttukey2g  9728  fundmge2nop0  13651  s4dom  14133  relexp0g  14232  relexpsucnnr  14235  dfrtrcl2  14272  ello1  14723  elo1  14734  bpolylem  15252  bpolyval  15253  isoval  16883  istsr  17675  islindf  20648  decpmatval0  21066  pmatcollpw3lem  21085  ordtval  21491  dfac14  21920  fmval  22245  fmf  22247  blfvalps  22686  tmsval  22784  cfilfval  23560  caufval  23571  isibl  24059  elcpn  24224  iscgrg  25990  uhgr0e  26549  incistruhgr  26557  ausgrusgri  26646  egrsubgr  26752  vtxdgfval  26942  vtxdg0e  26949  1egrvtxdg1  26984  eupth0  27733  ex-dm  27986  f1ocnt  30261  locfinreflem  30705  pstmval  30736  cntnevol  31089  omsval  31153  sitgval  31192  elprob  31270  cndprobval  31294  rrvmbfm  31303  bnj1385  31713  bnj1400  31716  bnj1014  31840  bnj1015  31841  bnj1326  31904  bnj1321  31905  bnj1491  31935  mrsubfval  32215  rdgprc0  32499  dfrdg2  32501  bdayval  32616  bdayfo  32643  noprefixmo  32663  nosupdm  32665  nosupfv  32667  nosupres  32668  nosupbnd1lem1  32669  nosupbnd1lem3  32671  nosupbnd1lem5  32673  nosupbnd2  32677  noetalem3  32680  brdomaing  32857  fwddifval  33084  fwddifnval  33085  filnetlem4  33190  cureq  34257  ismtyval  34468  isass  34514  isexid  34515  ismgmOLD  34518  elrefrels2  35150  elrefrels3  35151  refreleq  35153  elcnvrefrels2  35163  elcnvrefrels3  35164  elrefsymrels2  35198  eleqvrels2  35220  eleqvrels3  35221  dmqseq  35268  aomclem6  39000  aomclem8  39002  dfac21  39007  rclexi  39283  rtrclex  39285  rtrclexi  39289  cnvrcl0  39293  dfrtrcl5  39297  dfrcl2  39327  gneispace2  39790  ssnnf1octb  40826  sge0val  42025  ismea  42110  caragenval  42152  isome  42153  issmflem  42381  isomgreqve  43298  fnxpdmdm  43343  offval0  43872  elbigo  43919