MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dmeq Structured version   Visualization version   GIF version

Theorem dmeq 5740
Description: Equality theorem for domain. (Contributed by NM, 11-Aug-1994.)
Assertion
Ref Expression
dmeq (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)

Proof of Theorem dmeq
StepHypRef Expression
1 dmss 5739 . . 3 (𝐴𝐵 → dom 𝐴 ⊆ dom 𝐵)
2 dmss 5739 . . 3 (𝐵𝐴 → dom 𝐵 ⊆ dom 𝐴)
31, 2anim12i 615 . 2 ((𝐴𝐵𝐵𝐴) → (dom 𝐴 ⊆ dom 𝐵 ∧ dom 𝐵 ⊆ dom 𝐴))
4 eqss 3933 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
5 eqss 3933 . 2 (dom 𝐴 = dom 𝐵 ↔ (dom 𝐴 ⊆ dom 𝐵 ∧ dom 𝐵 ⊆ dom 𝐴))
63, 4, 53imtr4i 295 1 (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1538  wss 3884  dom cdm 5523
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-v 3446  df-un 3889  df-in 3891  df-ss 3901  df-sn 4529  df-pr 4531  df-op 4535  df-br 5034  df-dm 5533
This theorem is referenced by:  dmeqi  5741  dmeqd  5742  xpid11  5770  resresdm  6061  fneq1  6418  eqfnfv2  6784  funopdmsn  6893  nvof1o  7019  offval  7400  ofrfval  7401  offval3  7669  suppval  7819  smoeq  7974  tz7.44lem1  8028  tz7.44-2  8030  tz7.44-3  8031  ereq1  8283  fundmeng  8571  fseqenlem2  9440  dfac3  9536  dfac9  9551  dfac12lem1  9558  dfac12r  9561  ackbij2lem2  9655  ackbij2lem3  9656  r1om  9659  cfsmolem  9685  cfsmo  9686  dcomex  9862  axdc2lem  9863  axdc3lem2  9866  axdc3lem4  9868  ac7g  9889  ttukey2g  9931  fundmge2nop0  13850  s4dom  14276  relexp0g  14376  relexpsucnnr  14379  dfrtrcl2  14416  ello1  14867  elo1  14878  bpolylem  15397  bpolyval  15398  isoval  17030  istsr  17822  islindf  20504  decpmatval0  21372  pmatcollpw3lem  21391  ordtval  21797  dfac14  22226  fmval  22551  fmf  22553  blfvalps  22993  tmsval  23091  cfilfval  23871  caufval  23882  isibl  24372  elcpn  24540  iscgrg  26309  uhgr0e  26867  incistruhgr  26875  ausgrusgri  26964  egrsubgr  27070  vtxdgfval  27260  vtxdg0e  27267  1egrvtxdg1  27302  eupth0  28002  ex-dm  28227  eldmne0  30390  f1ocnt  30554  tocycfv  30804  tocycf  30812  tocyc01  30813  cycpmco2f1  30819  cycpmco2rn  30820  cycpmco2lem1  30821  cycpmco2lem2  30822  cycpmco2lem3  30823  cycpmco2lem4  30824  cycpmco2lem5  30825  cycpmco2lem6  30826  cycpmco2lem7  30827  cycpmco2  30828  cycpm3cl2  30831  cycpmconjv  30837  tocyccntz  30839  cyc3evpm  30845  cycpmgcl  30848  cycpmconjslem2  30850  cyc3conja  30852  locfinreflem  31193  pstmval  31246  cntnevol  31595  omsval  31659  sitgval  31698  elprob  31775  cndprobval  31799  rrvmbfm  31808  bnj1385  32212  bnj1400  32215  bnj1014  32341  bnj1015  32342  bnj1326  32406  bnj1321  32407  bnj1491  32437  mrsubfval  32863  rdgprc0  33146  dfrdg2  33148  bdayval  33263  bdayfo  33290  noprefixmo  33310  nosupdm  33312  nosupfv  33314  nosupres  33315  nosupbnd1lem1  33316  nosupbnd1lem3  33318  nosupbnd1lem5  33320  nosupbnd2  33324  noetalem3  33327  brdomaing  33504  fwddifval  33731  fwddifnval  33732  filnetlem4  33837  cureq  35026  ismtyval  35231  isass  35277  isexid  35278  ismgmOLD  35281  elrefrels2  35910  elrefrels3  35911  refreleq  35913  elcnvrefrels2  35923  elcnvrefrels3  35924  elrefsymrels2  35958  eleqvrels2  35980  eleqvrels3  35981  dmqseq  36028  aomclem6  39990  aomclem8  39992  dfac21  39997  rclexi  40302  rtrclex  40304  rtrclexi  40308  cnvrcl0  40312  dfrtrcl5  40316  dfrcl2  40362  gneispace2  40822  ssnnf1octb  41809  sge0val  42992  ismea  43077  caragenval  43119  isome  43120  issmflem  43348  isomgreqve  44330  fnxpdmdm  44375  elbigo  44952  itcoval  45062
  Copyright terms: Public domain W3C validator