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

Theorem eqimss 3345
Description: Equality implies the subclass relation. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)
Assertion
Ref Expression
eqimss  |-  ( A  =  B  ->  A  C_  B )

Proof of Theorem eqimss
StepHypRef Expression
1 eqss 3308 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
21simplbi 447 1  |-  ( A  =  B  ->  A  C_  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    C_ wss 3265
This theorem is referenced by:  eqimss2  3346  sspss  3391  uneqin  3537  uneqdifeq  3661  pwpw0  3891  sssn  3902  eqsn  3905  snsspw  3914  pwsnALT  3954  unissint  4018  elpwuni  4121  disjeq2  4129  disjeq1  4132  pwne  4309  pwssun  4432  poeq2  4450  freq2  4496  seeq1  4497  seeq2  4498  trsucss  4609  suc11  4627  suceloni  4735  frsn  4890  dmxpss  5242  xp11  5246  dmsnopss  5284  iotassuni  5376  funeq  5415  fnresdm  5496  fssxp  5544  ffdm  5547  fcoi1  5559  fof  5595  dff1o2  5621  fvmptss  5754  fvmptss2  5765  funressn  5860  dff1o6  5954  tposeq  6419  tfrlem11  6587  oewordi  6772  oewordri  6773  dffi3  7373  cantnfle  7561  cantnflem2  7581  r1ord3g  7640  rankeq0b  7721  rankxplim3  7740  carddom2  7799  cflm  8065  cfsuc  8072  isf32lem2  8169  axdc3lem2  8266  ttukeylem5  8328  tsksuc  8572  invf  13922  sscres  13952  pgpssslw  15177  fislw  15188  frgpup1  15336  frgpup3lem  15338  dprdspan  15514  dprdz  15517  dprdf1o  15519  dprd2da  15529  ablfac1b  15557  lspsncmp  16117  lspsnne2  16119  lspsneq  16123  psrbaglesupp  16362  psrbaglefi  16366  mplcoe2  16459  mplbas2  16460  istps2OLD  16911  cncnpi  17266  hauscmplem  17393  iskgen2  17503  elqtop3  17658  qtoprest  17672  hmeores  17726  snfil  17819  uffixfr  17878  ustuqtop2  18195  tngngp2  18566  metnrmlem3  18764  volcn  19367  recnprss  19660  plyeq0  19999  chsupsn  22765  chlejb1i  22828  atsseq  23700  difneqnul  23843  measxun2  24360  measssd  24365  measiuns  24367  funsseq  25151  ovoliunnfl  25955  voliunnfl  25957  volsupnfl  25958  opnbnd  26021  cldbnd  26022  fnemeet1  26088  heiborlem10  26222  smprngopr  26355  nacsfix  26459  psgnghm2  27109  dvconstbi  27222  bnj1143  28501  bnj1322  28534  lshpcmp  29105  lsatcmp  29120  lsatcmp2  29121  lshpset2N  29236  paddasslem17  29952  pcl0bN  30039  pexmidALTN  30094  lcfrlem26  31685  lcfrlem36  31695  mapd0  31782
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2376  df-cleq 2382  df-clel 2385  df-in 3272  df-ss 3279
  Copyright terms: Public domain W3C validator