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

Theorem eqimss 3400
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 3363 . 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 1652    C_ wss 3320
This theorem is referenced by:  eqimss2  3401  sspss  3446  uneqin  3592  uneqdifeq  3716  pwpw0  3946  sssn  3957  eqsn  3960  snsspw  3970  pwsnALT  4010  unissint  4074  elpwuni  4178  disjeq2  4186  disjeq1  4189  pwne  4366  pwssun  4489  poeq2  4507  freq2  4553  seeq1  4554  seeq2  4555  trsucss  4667  suc11  4685  suceloni  4793  frsn  4948  dmxpss  5300  xp11  5304  dmsnopss  5342  iotassuni  5434  funeq  5473  fnresdm  5554  fssxp  5602  ffdm  5605  fcoi1  5617  fof  5653  dff1o2  5679  fvmptss  5813  fvmptss2  5824  funressn  5919  dff1o6  6013  tposeq  6481  tfrlem11  6649  oewordi  6834  oewordri  6835  dffi3  7436  cantnfle  7626  cantnflem2  7646  r1ord3g  7705  rankeq0b  7786  rankxplim3  7805  carddom2  7864  cflm  8130  cfsuc  8137  isf32lem2  8234  axdc3lem2  8331  ttukeylem5  8393  tsksuc  8637  invf  13993  sscres  14023  pgpssslw  15248  fislw  15259  frgpup1  15407  frgpup3lem  15409  dprdspan  15585  dprdz  15588  dprdf1o  15590  dprd2da  15600  ablfac1b  15628  lspsncmp  16188  lspsnne2  16190  lspsneq  16194  psrbaglesupp  16433  psrbaglefi  16437  mplcoe2  16530  mplbas2  16531  istps2OLD  16986  cncnpi  17342  hauscmplem  17469  iskgen2  17580  elqtop3  17735  qtoprest  17749  hmeores  17803  snfil  17896  uffixfr  17955  ustuqtop2  18272  tngngp2  18693  metnrmlem3  18891  volcn  19498  recnprss  19791  plyeq0  20130  chsupsn  22915  chlejb1i  22978  atsseq  23850  difneqnul  23997  measxun2  24564  measssd  24569  measiuns  24571  funsseq  25393  ovoliunnfl  26248  voliunnfl  26250  volsupnfl  26251  opnbnd  26328  cldbnd  26329  fnemeet1  26395  heiborlem10  26529  smprngopr  26662  nacsfix  26766  psgnghm2  27415  dvconstbi  27528  bnj1143  29161  bnj1322  29194  lshpcmp  29786  lsatcmp  29801  lsatcmp2  29802  lshpset2N  29917  paddasslem17  30633  pcl0bN  30720  pexmidALTN  30775  lcfrlem26  32366  lcfrlem36  32376  mapd0  32463
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-in 3327  df-ss 3334
  Copyright terms: Public domain W3C validator