Theorem dmeq 5825

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

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1539   ⊆ wss 3892  dom cdm 5600

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3287  df-v 3439  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4566  df-pr 4568  df-op 4572  df-br 5082  df-dm 5610

This theorem is referenced by:  dmeqi  5826  dmeqd  5827  xpid11  5853  resresdm  6151  fneq1  6555  eqfnfv2  6942  funopdmsn  7054  nvof1o  7184  ofrfvalg  7573  offval  7574  offval3  7857  suppval  8010  smoeq  8212  tz7.44lem1  8267  tz7.44-2  8269  tz7.44-3  8270  ereq1  8536  fundmeng  8857  fseqenlem2  9827  dfac3  9923  dfac9  9938  dfac12lem1  9945  dfac12r  9948  ackbij2lem2  10042  ackbij2lem3  10043  r1om  10046  cfsmolem  10072  cfsmo  10073  dcomex  10249  axdc2lem  10250  axdc3lem2  10253  axdc3lem4  10255  ac7g  10276  ttukey2g  10318  fundmge2nop0  14251  s4dom  14677  relexp0g  14778  relexpsucnnr  14781  dfrtrcl2  14818  ello1  15269  elo1  15280  bpolylem  15803  bpolyval  15804  isoval  17522  istsr  18346  islindf  21064  decpmatval0  21958  pmatcollpw3lem  21977  ordtval  22385  dfac14  22814  fmval  23139  fmf  23141  blfvalps  23581  tmsval  23681  cfilfval  24473  caufval  24484  isibl  24975  elcpn  25143  iscgrg  26918  uhgr0e  27486  incistruhgr  27494  ausgrusgri  27583  egrsubgr  27689  vtxdgfval  27879  vtxdg0e  27886  1egrvtxdg1  27921  eupth0  28623  ex-dm  28848  eldmne0  31008  f1ocnt  31168  tocycfv  31421  tocycf  31429  tocyc01  31430  cycpmco2f1  31436  cycpmco2rn  31437  cycpmco2lem1  31438  cycpmco2lem2  31439  cycpmco2lem3  31440  cycpmco2lem4  31441  cycpmco2lem5  31442  cycpmco2lem6  31443  cycpmco2lem7  31444  cycpmco2  31445  cycpm3cl2  31448  cycpmconjv  31454  tocyccntz  31456  cyc3evpm  31462  cycpmgcl  31465  cycpmconjslem2  31467  cyc3conja  31469  locfinreflem  31835  pstmval  31890  cntnevol  32241  omsval  32305  sitgval  32344  elprob  32421  cndprobval  32445  rrvmbfm  32454  bnj1385  32857  bnj1400  32860  bnj1014  32986  bnj1015  32987  bnj1326  33051  bnj1321  33052  bnj1491  33082  fineqvac  33111  mrsubfval  33515  rdgprc0  33814  dfrdg2  33816  bdayval  33896  bdayfo  33925  nosupprefixmo  33948  noinfprefixmo  33949  nosupcbv  33950  nosupdm  33952  nosupfv  33954  nosupres  33955  nosupbnd1lem1  33956  nosupbnd1lem3  33958  nosupbnd1lem5  33960  nosupbnd2  33964  noinfcbv  33965  noinfdm  33967  noinffv  33969  noinfres  33970  noinfbnd1lem3  33973  noinfbnd1lem5  33975  noetasuplem4  33984  noetainflem4  33988  brdomaing  34282  fwddifval  34509  fwddifnval  34510  filnetlem4  34615  cureq  35797  ismtyval  36002  isass  36048  isexid  36049  ismgmOLD  36052  elrefrels2  36677  elrefrels3  36678  refreleq  36680  elcnvrefrels2  36690  elcnvrefrels3  36691  elrefsymrels2  36725  eleqvrels2  36747  eleqvrels3  36748  dmqseq  36795  aomclem6  40922  aomclem8  40924  dfac21  40929  rclexi  41261  rtrclex  41263  rtrclexi  41267  cnvrcl0  41271  dfrtrcl5  41275  dfrcl2  41320  gneispace2  41780  ssnnf1octb  42777  sge0val  43954  ismea  44039  caragenval  44081  isome  44082  issmflem  44315  isomgreqve  45335  fnxpdmdm  45380  elbigo  45955  itcoval  46065