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

Theorem eqimss 3232
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 3196 . 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 1625    C_ wss 3154
This theorem is referenced by:  eqimss2  3233  sspss  3277  uneqin  3422  uneqdifeq  3544  pwpw0  3765  sssn  3774  eqsn  3777  snsspw  3786  pwsnALT  3824  unissint  3888  elpwuni  3991  disjeq2  3999  disjeq1  4002  pwne  4179  pwssun  4301  poeq2  4320  freq2  4366  seeq1  4367  seeq2  4368  trsucss  4480  suc11  4498  suceloni  4606  frsn  4762  dmxpss  5109  xp11  5113  dmsnopss  5147  iotassuni  5237  funeq  5276  fnresdm  5355  fssxp  5402  ffdm  5405  fcoi1  5417  fof  5453  dff1o2  5479  fvmptss  5611  fvmptss2  5621  funressn  5708  dff1o6  5793  tposeq  6238  tfrlem11  6406  oewordi  6591  oewordri  6592  dffi3  7186  cantnfle  7374  cantnflem2  7394  r1ord3g  7453  rankeq0b  7534  rankxplim3  7553  carddom2  7612  cflm  7878  cfsuc  7885  isf32lem2  7982  axdc3lem2  8079  ttukeylem5  8142  tsksuc  8386  invf  13672  sscres  13702  pgpssslw  14927  fislw  14938  frgpup1  15086  frgpup3lem  15088  dprdspan  15264  dprdz  15267  dprdf1o  15269  dprd2da  15279  ablfac1b  15307  lspsncmp  15871  lspsnne2  15873  lspsneq  15877  psrbaglesupp  16116  psrbaglefi  16120  mplcoe2  16213  mplbas2  16214  istps2OLD  16661  cncnpi  17009  hauscmplem  17135  iskgen2  17245  elqtop3  17396  qtoprest  17410  hmeores  17464  snfil  17561  uffixfr  17620  tngngp2  18170  metnrmlem3  18367  volcn  18963  recnprss  19256  plyeq0  19595  chsupsn  21994  chlejb1i  22057  atsseq  22929  difneqnul  23129  measxun2  23540  measssd  23545  indf1ofs  23611  funsseq  24127  dfps2  25300  basexre  25533  trnij  25626  prismorcsetlemc  25928  opnbnd  26254  cldbnd  26255  fnemeet1  26326  heiborlem10  26555  smprngopr  26688  nacsfix  26798  psgnghm2  27449  dvconstbi  27562  bnj1143  28895  bnj1322  28928  lshpcmp  29251  lsatcmp  29266  lsatcmp2  29267  lshpset2N  29382  paddasslem17  30098  pcl0bN  30185  pexmidALTN  30240  lcfrlem26  31831  lcfrlem36  31841  mapd0  31928
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-in 3161  df-ss 3168
  Copyright terms: Public domain W3C validator