Theorem eqimss 3494

Description: Equality implies the subclass relation. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)

Assertion

Ref	Expression
eqimss	|- ( A = B -> A C_ B )

Proof of Theorem eqimss

Step	Hyp	Ref	Expression
1		eqss 3457	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
2	1	simplbi 458	1 |- ( A = B -> A C_ B )

Syntax hints:   -> wi 4   = wceq 1405   C_ wss 3414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-in 3421  df-ss 3428

This theorem is referenced by:  eqimss2  3495  sspss  3542  uneqin  3701  difn0  3829  uneqdifeq  3860  pwpw0  4120  sssn  4130  eqsn  4133  snsspw  4143  pwsnALT  4186  unissint  4252  elpwuni  4362  disjeq2  4370  disjeq1  4373  pwne  4560  pwssun  4729  poeq2  4748  freq2  4794  seeq1  4795  seeq2  4796  frsn  4894  dmxpss  5256  xp11  5260  dmsnopss  5296  trsucss  5495  suc11  5513  iotassuni  5549  funeq  5588  fnresdm  5671  fssxp  5726  ffdm  5728  fcoi1  5742  fof  5778  dff1o2  5804  fvmptss  5942  fvmptss2  5953  funressn  6064  dff1o6  6162  suceloni  6631  tposeq  6960  tfrlem11  7091  oewordi  7277  oewordri  7278  dffi3  7925  cantnfle  8122  cantnflem2  8141  cantnfleOLD  8152  r1ord3g  8229  rankeq0b  8310  rankxplim3  8331  carddom2  8390  cflm  8662  cfsuc  8669  isf32lem2  8766  axdc3lem2  8863  ttukeylem5  8925  tsksuc  9170  fsuppmapnn0fiublem  12140  fsuppmapnn0fiub  12141  xptrrel  12963  relexpnndm  13023  relexpdmg  13024  relexprng  13028  relexpfld  13031  relexpaddg  13035  invf  15381  sscres  15436  pgpssslw  16958  fislw  16969  frgpup1  17117  frgpup3lem  17119  dprdspan  17394  dprdz  17397  dprdf1o  17399  dprd2da  17411  ablfac1b  17441  lspsncmp  18082  lspsnne2  18084  lspsneq  18088  psrbaglesupp  18337  psrbaglesuppOLD  18338  psrbaglefi  18343  psrbaglefiOLD  18344  mplcoe5  18451  mplcoe2OLD  18453  mplbas2  18454  mplbas2OLD  18455  psgnghm2  18915  ofco2  19245  istps2OLD  19714  cncnpi  20072  hauscmplem  20199  iskgen2  20341  elqtop3  20496  qtoprest  20510  hmeores  20564  snfil  20657  uffixfr  20716  ustuqtop2  21037  tngngp2  21458  metnrmlem3  21657  volcn  22307  recnprss  22600  plyeq0  22900  chsupsn  26745  chlejb1i  26808  atsseq  27679  disjeq1f  27866  ldgenpisys  28614  measxun2  28658  measssd  28663  measiuns  28665  pmeasmono  28772  eulerpartlemb  28813  bnj1143  29176  bnj1322  29208  funsseq  29982  opnbnd  30553  cldbnd  30554  fnemeet1  30594  relowlpssretop  31281  ovoliunnfl  31428  voliunnfl  31430  volsupnfl  31431  heiborlem10  31598  smprngopr  31731  lshpcmp  32006  lsatcmp  32021  lsatcmp2  32022  lshpset2N  32137  paddasslem17  32853  pcl0bN  32940  pexmidALTN  32995  lcfrlem26  34588  lcfrlem36  34598  mapd0  34685  nacsfix  35006  cbviuneq12df  35640  relexp0a  35695  relexpaddss  35697  frege124d  35740  dvconstbi  36087  icccncfext  37058  dvmptconst  37078  dvmptidg  37080  dvmulcncf  37090  dvdivcncf  37092  dirkercncflem2  37254  fourierdlem70  37327  fourierdlem71  37328