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

Theorem eqimss 3392
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 3355 . 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 3312
This theorem is referenced by:  eqimss2  3393  sspss  3438  uneqin  3584  uneqdifeq  3708  pwpw0  3938  sssn  3949  eqsn  3952  snsspw  3962  pwsnALT  4002  unissint  4066  elpwuni  4170  disjeq2  4178  disjeq1  4181  pwne  4358  pwssun  4481  poeq2  4499  freq2  4545  seeq1  4546  seeq2  4547  trsucss  4659  suc11  4677  suceloni  4785  frsn  4940  dmxpss  5292  xp11  5296  dmsnopss  5334  iotassuni  5426  funeq  5465  fnresdm  5546  fssxp  5594  ffdm  5597  fcoi1  5609  fof  5645  dff1o2  5671  fvmptss  5805  fvmptss2  5816  funressn  5911  dff1o6  6005  tposeq  6473  tfrlem11  6641  oewordi  6826  oewordri  6827  dffi3  7428  cantnfle  7618  cantnflem2  7638  r1ord3g  7697  rankeq0b  7778  rankxplim3  7797  carddom2  7856  cflm  8122  cfsuc  8129  isf32lem2  8226  axdc3lem2  8323  ttukeylem5  8385  tsksuc  8629  invf  13985  sscres  14015  pgpssslw  15240  fislw  15251  frgpup1  15399  frgpup3lem  15401  dprdspan  15577  dprdz  15580  dprdf1o  15582  dprd2da  15592  ablfac1b  15620  lspsncmp  16180  lspsnne2  16182  lspsneq  16186  psrbaglesupp  16425  psrbaglefi  16429  mplcoe2  16522  mplbas2  16523  istps2OLD  16978  cncnpi  17334  hauscmplem  17461  iskgen2  17572  elqtop3  17727  qtoprest  17741  hmeores  17795  snfil  17888  uffixfr  17947  ustuqtop2  18264  tngngp2  18685  metnrmlem3  18883  volcn  19490  recnprss  19783  plyeq0  20122  chsupsn  22907  chlejb1i  22970  atsseq  23842  difneqnul  23989  measxun2  24556  measssd  24561  measiuns  24563  funsseq  25385  ovoliunnfl  26238  voliunnfl  26240  volsupnfl  26241  opnbnd  26319  cldbnd  26320  fnemeet1  26386  heiborlem10  26520  smprngopr  26653  nacsfix  26757  psgnghm2  27406  dvconstbi  27519  bnj1143  29098  bnj1322  29131  lshpcmp  29723  lsatcmp  29738  lsatcmp2  29739  lshpset2N  29854  paddasslem17  30570  pcl0bN  30657  pexmidALTN  30712  lcfrlem26  32303  lcfrlem36  32313  mapd0  32400
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 2416
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 2422  df-cleq 2428  df-clel 2431  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator