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

Theorem eqimss 3316
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 3280 . 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 1647    C_ wss 3238
This theorem is referenced by:  eqimss2  3317  sspss  3362  uneqin  3508  uneqdifeq  3631  pwpw0  3861  sssn  3872  eqsn  3875  snsspw  3884  pwsnALT  3924  unissint  3988  elpwuni  4091  disjeq2  4099  disjeq1  4102  pwne  4279  pwssun  4402  poeq2  4421  freq2  4467  seeq1  4468  seeq2  4469  trsucss  4581  suc11  4599  suceloni  4707  frsn  4863  dmxpss  5210  xp11  5214  dmsnopss  5248  iotassuni  5338  funeq  5377  fnresdm  5458  fssxp  5506  ffdm  5509  fcoi1  5521  fof  5557  dff1o2  5583  fvmptss  5716  fvmptss2  5726  funressn  5819  dff1o6  5913  tposeq  6378  tfrlem11  6546  oewordi  6731  oewordri  6732  dffi3  7331  cantnfle  7519  cantnflem2  7539  r1ord3g  7598  rankeq0b  7679  rankxplim3  7698  carddom2  7757  cflm  8023  cfsuc  8030  isf32lem2  8127  axdc3lem2  8224  ttukeylem5  8287  tsksuc  8531  invf  13880  sscres  13910  pgpssslw  15135  fislw  15146  frgpup1  15294  frgpup3lem  15296  dprdspan  15472  dprdz  15475  dprdf1o  15477  dprd2da  15487  ablfac1b  15515  lspsncmp  16079  lspsnne2  16081  lspsneq  16085  psrbaglesupp  16324  psrbaglefi  16328  mplcoe2  16421  mplbas2  16422  istps2OLD  16876  cncnpi  17224  hauscmplem  17350  iskgen2  17460  elqtop3  17611  qtoprest  17625  hmeores  17679  snfil  17772  uffixfr  17831  tngngp2  18381  metnrmlem3  18579  volcn  19176  recnprss  19469  plyeq0  19808  chsupsn  22426  chlejb1i  22489  atsseq  23361  difneqnul  23515  ustuqtop2  23866  indf1ofs  24009  measxun2  24148  measssd  24153  funsseq  24951  ovoliunnfl  25756  voliunnfl  25758  volsupnfl  25759  opnbnd  25835  cldbnd  25836  fnemeet1  25907  heiborlem10  26135  smprngopr  26268  nacsfix  26378  psgnghm2  27029  dvconstbi  27142  bnj1143  28574  bnj1322  28607  lshpcmp  29237  lsatcmp  29252  lsatcmp2  29253  lshpset2N  29368  paddasslem17  30084  pcl0bN  30171  pexmidALTN  30226  lcfrlem26  31817  lcfrlem36  31827  mapd0  31914
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-in 3245  df-ss 3252
  Copyright terms: Public domain W3C validator