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

Theorem eqimss 3230
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 3194 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
21simplbi 446 1  |-  ( A  =  B  ->  A  C_  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    C_ wss 3152
This theorem is referenced by:  eqimss2  3231  sspss  3275  uneqin  3420  uneqdifeq  3542  pwpw0  3763  sssn  3772  eqsn  3775  snsspw  3784  pwsnALT  3822  unissint  3886  elpwuni  3989  disjeq2  3997  disjeq1  4000  pwne  4177  pwssun  4299  poeq2  4318  freq2  4364  seeq1  4365  seeq2  4366  trsucss  4478  suc11  4496  suceloni  4604  frsn  4760  dmxpss  5107  xp11  5111  dmsnopss  5145  iotassuni  5235  funeq  5274  fnresdm  5353  fssxp  5400  ffdm  5403  fcoi1  5415  fof  5451  dff1o2  5477  fvmptss  5609  fvmptss2  5619  funressn  5706  dff1o6  5791  tposeq  6236  tfrlem11  6404  oewordi  6589  oewordri  6590  dffi3  7184  cantnfle  7372  cantnflem2  7392  r1ord3g  7451  rankeq0b  7532  rankxplim3  7551  carddom2  7610  cflm  7876  cfsuc  7883  isf32lem2  7980  axdc3lem2  8077  ttukeylem5  8140  tsksuc  8384  invf  13670  sscres  13700  pgpssslw  14925  fislw  14936  frgpup1  15084  frgpup3lem  15086  dprdspan  15262  dprdz  15265  dprdf1o  15267  dprd2da  15277  ablfac1b  15305  lspsncmp  15869  lspsnne2  15871  lspsneq  15875  psrbaglesupp  16114  psrbaglefi  16118  mplcoe2  16211  mplbas2  16212  istps2OLD  16659  cncnpi  17007  hauscmplem  17133  iskgen2  17243  elqtop3  17394  qtoprest  17408  hmeores  17462  snfil  17559  uffixfr  17618  tngngp2  18168  metnrmlem3  18365  volcn  18961  recnprss  19254  plyeq0  19593  chsupsn  21992  chlejb1i  22055  atsseq  22927  difneqnul  23127  measxun2  23538  measssd  23543  indf1ofs  23609  funsseq  24125  dfps2  25289  basexre  25522  trnij  25615  prismorcsetlemc  25917  opnbnd  26243  cldbnd  26244  fnemeet1  26315  heiborlem10  26544  smprngopr  26677  nacsfix  26787  psgnghm2  27438  dvconstbi  27551  bnj1143  28822  bnj1322  28855  lshpcmp  29178  lsatcmp  29193  lsatcmp2  29194  lshpset2N  29309  paddasslem17  30025  pcl0bN  30112  pexmidALTN  30167  lcfrlem26  31758  lcfrlem36  31768  mapd0  31855
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator