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

Theorem eqimss 3360
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 3323 . 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 1649    C_ wss 3280
This theorem is referenced by:  eqimss2  3361  sspss  3406  uneqin  3552  uneqdifeq  3676  pwpw0  3906  sssn  3917  eqsn  3920  snsspw  3930  pwsnALT  3970  unissint  4034  elpwuni  4138  disjeq2  4146  disjeq1  4149  pwne  4326  pwssun  4449  poeq2  4467  freq2  4513  seeq1  4514  seeq2  4515  trsucss  4626  suc11  4644  suceloni  4752  frsn  4907  dmxpss  5259  xp11  5263  dmsnopss  5301  iotassuni  5393  funeq  5432  fnresdm  5513  fssxp  5561  ffdm  5564  fcoi1  5576  fof  5612  dff1o2  5638  fvmptss  5772  fvmptss2  5783  funressn  5878  dff1o6  5972  tposeq  6440  tfrlem11  6608  oewordi  6793  oewordri  6794  dffi3  7394  cantnfle  7582  cantnflem2  7602  r1ord3g  7661  rankeq0b  7742  rankxplim3  7761  carddom2  7820  cflm  8086  cfsuc  8093  isf32lem2  8190  axdc3lem2  8287  ttukeylem5  8349  tsksuc  8593  invf  13948  sscres  13978  pgpssslw  15203  fislw  15214  frgpup1  15362  frgpup3lem  15364  dprdspan  15540  dprdz  15543  dprdf1o  15545  dprd2da  15555  ablfac1b  15583  lspsncmp  16143  lspsnne2  16145  lspsneq  16149  psrbaglesupp  16388  psrbaglefi  16392  mplcoe2  16485  mplbas2  16486  istps2OLD  16941  cncnpi  17296  hauscmplem  17423  iskgen2  17533  elqtop3  17688  qtoprest  17702  hmeores  17756  snfil  17849  uffixfr  17908  ustuqtop2  18225  tngngp2  18646  metnrmlem3  18844  volcn  19451  recnprss  19744  plyeq0  20083  chsupsn  22868  chlejb1i  22931  atsseq  23803  difneqnul  23950  measxun2  24517  measssd  24522  measiuns  24524  funsseq  25339  ovoliunnfl  26147  voliunnfl  26149  volsupnfl  26150  opnbnd  26218  cldbnd  26219  fnemeet1  26285  heiborlem10  26419  smprngopr  26552  nacsfix  26656  psgnghm2  27306  dvconstbi  27419  bnj1143  28867  bnj1322  28900  lshpcmp  29471  lsatcmp  29486  lsatcmp2  29487  lshpset2N  29602  paddasslem17  30318  pcl0bN  30405  pexmidALTN  30460  lcfrlem26  32051  lcfrlem36  32061  mapd0  32148
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-in 3287  df-ss 3294
  Copyright terms: Public domain W3C validator