Theorem eqimss 3538

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 3501	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
2	1	simplbi 460	1 |- ( A = B -> A C_ B )

Syntax hints:   -> wi 4   = wceq 1381   C_ wss 3458

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-in 3465  df-ss 3472

This theorem is referenced by:  eqimss2  3539  sspss  3585  uneqin  3731  uneqdifeq  3898  pwpw0  4159  sssn  4169  eqsn  4172  snsspw  4182  pwsnALT  4225  unissint  4292  elpwuni  4399  disjeq2  4407  disjeq1  4410  pwne  4599  pwssun  4772  poeq2  4790  freq2  4836  seeq1  4837  seeq2  4838  trsucss  4949  suc11  4967  frsn  5056  dmxpss  5424  xp11  5428  dmsnopss  5466  iotassuni  5553  funeq  5593  fnresdm  5676  fssxp  5729  ffdm  5731  fcoi1  5745  fof  5781  dff1o2  5807  fvmptss  5945  fvmptss2  5956  funressn  6065  dff1o6  6162  suceloni  6629  tposeq  6955  tfrlem11  7055  oewordi  7238  oewordri  7239  dffi3  7889  cantnfle  8088  cantnflem2  8107  cantnfleOLD  8118  r1ord3g  8195  rankeq0b  8276  rankxplim3  8297  carddom2  8356  cflm  8628  cfsuc  8635  isf32lem2  8732  axdc3lem2  8829  ttukeylem5  8891  tsksuc  9138  fsuppmapnn0fiublem  12070  fsuppmapnn0fiub  12071  invf  15034  sscres  15064  pgpssslw  16503  fislw  16514  frgpup1  16662  frgpup3lem  16664  dprdspan  16942  dprdz  16945  dprdf1o  16947  dprd2da  16959  ablfac1b  16989  lspsncmp  17630  lspsnne2  17632  lspsneq  17636  psrbaglesupp  17885  psrbaglesuppOLD  17886  psrbaglefi  17891  psrbaglefiOLD  17892  mplcoe5  17999  mplcoe2OLD  18001  mplbas2  18002  mplbas2OLD  18003  psgnghm2  18484  ofco2  18820  istps2OLD  19289  cncnpi  19645  hauscmplem  19772  iskgen2  19915  elqtop3  20070  qtoprest  20084  hmeores  20138  snfil  20231  uffixfr  20290  ustuqtop2  20611  tngngp2  21032  metnrmlem3  21231  volcn  21881  recnprss  22174  plyeq0  22474  chsupsn  26196  chlejb1i  26259  atsseq  27131  difneqnul  27280  measxun2  28047  measssd  28052  measiuns  28054  eulerpartlemb  28173  funsseq  29167  ovoliunnfl  30024  voliunnfl  30026  volsupnfl  30027  opnbnd  30111  cldbnd  30112  fnemeet1  30152  heiborlem10  30284  smprngopr  30417  nacsfix  30612  dvconstbi  31208  icccncfext  31593  dvmptconst  31610  dvmptidg  31612  dvmulcncf  31622  dvdivcncf  31624  dirkercncflem2  31771  fourierdlem70  31844  fourierdlem71  31845  bnj1143  33556  bnj1322  33588  lshpcmp  34415  lsatcmp  34430  lsatcmp2  34431  lshpset2N  34546  paddasslem17  35262  pcl0bN  35349  pexmidALTN  35404  lcfrlem26  36997  lcfrlem36  37007  mapd0  37094  xptrrel  37430