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

Theorem eqimss 3786
Description: Equality implies the subclass relation. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)
Assertion
Ref Expression
eqimss (𝐴 = 𝐵𝐴𝐵)

Proof of Theorem eqimss
StepHypRef Expression
1 eqss 3747 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
21simplbi 478 1 (𝐴 = 𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1620  wss 3703
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-clab 2735  df-cleq 2741  df-clel 2744  df-in 3710  df-ss 3717
This theorem is referenced by:  eqimss2  3787  sspss  3836  uneqin  4009  difn0  4074  ssdisj  4158  uneqdifeq  4189  uneqdifeqOLD  4190  pwpw0  4477  ssprsseq  4490  sssn  4491  eqsnOLD  4495  snsspw  4508  pwsnALT  4569  unissint  4641  pwpwssunieq  4755  elpwuni  4756  disjeq2  4764  disjeq1  4767  pwne  4968  pwssun  5158  poeq2  5179  freq2  5225  seeq1  5226  seeq2  5227  frsn  5334  dmxpss  5711  xp11  5715  dmsnopss  5754  trsucss  5960  suc11  5980  iotassuni  6016  funeq  6057  fnresdm  6149  fssxp  6209  ffdm  6211  fcoi1  6227  fof  6264  dff1o2  6291  fvmptss  6442  fvmptss2  6454  funressn  6577  dff1o6  6682  suceloni  7166  tposeq  7511  tfrlem11  7641  oewordi  7828  oewordri  7829  dffi3  8490  cantnfle  8729  cantnflem2  8748  r1ord3g  8803  rankeq0b  8884  rankxplim3  8905  carddom2  8964  cflm  9235  cfsuc  9242  isf32lem2  9339  axdc3lem2  9436  ttukeylem5  9498  tsksuc  9747  fsuppmapnn0fiublem  12954  fsuppmapnn0fiub  12955  fsuppmapnn0fiubOLD  12956  xptrrel  13891  relexpnndm  13951  relexpdmg  13952  relexprng  13956  relexpfld  13959  relexpaddg  13963  invf  16600  sscres  16655  pgpssslw  18200  fislw  18211  frgpup1  18359  frgpup3lem  18361  dprdspan  18597  dprdz  18600  dprdf1o  18602  dprd2da  18612  ablfac1b  18640  lspsncmp  19289  lspsnne2  19291  lspsneq  19295  psrbaglesupp  19541  psrbaglefi  19545  mplcoe5  19641  mplbas2  19643  psgnghm2  20100  ofco2  20430  toprntopon  20902  cncnpi  21255  hauscmplem  21382  iskgen2  21524  elqtop3  21679  qtoprest  21693  hmeores  21747  snfil  21840  uffixfr  21899  ustuqtop2  22218  tngngp2  22628  metnrmlem3  22836  volcn  23545  recnprss  23838  plyeq0  24137  uhgr3cyclex  27305  chsupsn  28552  chlejb1i  28615  atsseq  29486  disjeq1f  29665  ldgenpisys  30509  measxun2  30553  measssd  30558  measiuns  30560  pmeasmono  30666  eulerpartlemb  30710  bnj1143  31139  bnj1322  31171  funsseq  31944  opnbnd  32597  cldbnd  32598  fnemeet1  32638  bj-restuni  33327  relowlpssretop  33494  ovoliunnfl  33733  voliunnfl  33735  volsupnfl  33736  heiborlem10  33901  smprngopr  34133  lshpcmp  34747  lsatcmp  34762  lsatcmp2  34763  lshpset2N  34878  paddasslem17  35594  pcl0bN  35681  pexmidALTN  35736  lcfrlem26  37328  lcfrlem36  37338  mapd0  37425  nacsfix  37746  cbviuneq12df  38424  relexp0a  38479  relexpaddss  38481  frege124d  38524  k0004lem3  38918  dvconstbi  39004  ssin0  39691  icccncfext  40572  dvmptconst  40601  dvmptidg  40603  dvmulcncf  40612  dvdivcncf  40614  dirkercncflem2  40793  fourierdlem70  40865  fourierdlem71  40866  hoicvr  41237  ovnsubaddlem1  41259  ovnhoi  41292  hspdifhsp  41305  0setrec  42929
  Copyright terms: Public domain W3C validator