Theorem dmeq 5928

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 5927	. . 3 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)
2		dmss 5927	. . 3 ⊢ (𝐵 ⊆ 𝐴 → dom 𝐵 ⊆ dom 𝐴)
3	1, 2	anim12i 612	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (dom 𝐴 ⊆ dom 𝐵 ∧ dom 𝐵 ⊆ dom 𝐴))
4		eqss 4024	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
5		eqss 4024	. 2 ⊢ (dom 𝐴 = dom 𝐵 ↔ (dom 𝐴 ⊆ dom 𝐵 ∧ dom 𝐵 ⊆ dom 𝐴))
6	3, 4, 5	3imtr4i 292	1 ⊢ (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ⊆ wss 3976  dom cdm 5700

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-dm 5710

This theorem is referenced by:  dmeqi  5929  dmeqd  5930  xpid11  5957  resresdm  6264  fneq1  6670  eqfnfv2  7065  funopdmsn  7184  nvof1o  7316  ofrfvalg  7722  offval  7723  offval3  8023  suppval  8203  smoeq  8406  tz7.44lem1  8461  tz7.44-2  8463  tz7.44-3  8464  ereq1  8770  fundmeng  9097  fseqenlem2  10094  dfac3  10190  dfac9  10206  dfac12lem1  10213  dfac12r  10216  ackbij2lem2  10308  ackbij2lem3  10309  r1om  10312  cfsmolem  10339  cfsmo  10340  dcomex  10516  axdc2lem  10517  axdc3lem2  10520  axdc3lem4  10522  ac7g  10543  ttukey2g  10585  fundmge2nop0  14551  s4dom  14968  relexp0g  15071  relexpsucnnr  15074  dfrtrcl2  15111  ello1  15561  elo1  15572  bpolylem  16096  bpolyval  16097  isoval  17826  istsr  18653  islindf  21855  decpmatval0  22791  pmatcollpw3lem  22810  ordtval  23218  dfac14  23647  fmval  23972  fmf  23974  blfvalps  24414  tmsval  24514  cfilfval  25317  caufval  25328  isibl  25820  elcpn  25990  bdayval  27711  bdayfo  27740  nosupprefixmo  27763  noinfprefixmo  27764  nosupcbv  27765  nosupdm  27767  nosupfv  27769  nosupres  27770  nosupbnd1lem1  27771  nosupbnd1lem3  27773  nosupbnd1lem5  27775  nosupbnd2  27779  noinfcbv  27780  noinfdm  27782  noinffv  27784  noinfres  27785  noinfbnd1lem3  27788  noinfbnd1lem5  27790  noetasuplem4  27799  noetainflem4  27803  iscgrg  28538  uhgr0e  29106  incistruhgr  29114  ausgrusgri  29203  egrsubgr  29312  vtxdgfval  29503  vtxdg0e  29510  1egrvtxdg1  29545  eupth0  30246  ex-dm  30471  eldmne0  32647  of0r  32696  f1ocnt  32807  ischn  32979  chnind  32983  tocycfv  33102  tocycf  33110  tocyc01  33111  cycpmco2f1  33117  cycpmco2rn  33118  cycpmco2lem1  33119  cycpmco2lem2  33120  cycpmco2lem3  33121  cycpmco2lem4  33122  cycpmco2lem5  33123  cycpmco2lem6  33124  cycpmco2lem7  33125  cycpmco2  33126  cycpm3cl2  33129  cycpmconjv  33135  tocyccntz  33137  cyc3evpm  33143  cycpmgcl  33146  cycpmconjslem2  33148  cyc3conja  33150  locfinreflem  33786  pstmval  33841  cntnevol  34192  omsval  34258  sitgval  34297  elprob  34374  cndprobval  34398  rrvmbfm  34407  bnj1385  34808  bnj1400  34811  bnj1014  34937  bnj1015  34938  bnj1326  35002  bnj1321  35003  bnj1491  35033  fineqvac  35073  mrsubfval  35476  rdgprc0  35757  dfrdg2  35759  brdomaing  35899  fwddifval  36126  fwddifnval  36127  filnetlem4  36347  cureq  37556  ismtyval  37760  isass  37806  isexid  37807  ismgmOLD  37810  elrefrels2  38474  elrefrels3  38475  refreleq  38477  elcnvrefrels2  38490  elcnvrefrels3  38491  elrefsymrels2  38525  eleqvrels2  38548  eleqvrels3  38549  dmqseq  38596  aomclem6  43016  aomclem8  43018  dfac21  43023  tfsconcatun  43299  tfsconcat0b  43308  tfsconcatrev  43310  rclexi  43577  rtrclex  43579  rtrclexi  43583  cnvrcl0  43587  dfrtrcl5  43591  dfrcl2  43636  gneispace2  44094  ssnnf1octb  45101  sge0val  46287  ismea  46372  caragenval  46414  isome  46415  issmflem  46648  isisubgr  47734  isgrim  47752  fnxpdmdm  47883  elbigo  48285  itcoval  48395