Theorem eqimss 3551

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

Syntax hints:   -> wi 4   = wceq 1395   C_ wss 3471

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3478  df-ss 3485

This theorem is referenced by:  eqimss2  3552  sspss  3599  uneqin  3756  uneqdifeq  3919  pwpw0  4180  sssn  4190  eqsn  4193  snsspw  4203  pwsnALT  4246  unissint  4313  elpwuni  4423  disjeq2  4431  disjeq1  4434  pwne  4622  pwssun  4795  poeq2  4813  freq2  4859  seeq1  4860  seeq2  4861  trsucss  4972  suc11  4990  frsn  5079  dmxpss  5445  xp11  5449  dmsnopss  5486  iotassuni  5573  funeq  5613  fnresdm  5696  fssxp  5749  ffdm  5751  fcoi1  5765  fof  5801  dff1o2  5827  fvmptss  5965  fvmptss2  5976  funressn  6085  dff1o6  6182  suceloni  6647  tposeq  6975  tfrlem11  7075  oewordi  7258  oewordri  7259  dffi3  7909  cantnfle  8107  cantnflem2  8126  cantnfleOLD  8137  r1ord3g  8214  rankeq0b  8295  rankxplim3  8316  carddom2  8375  cflm  8647  cfsuc  8654  isf32lem2  8751  axdc3lem2  8848  ttukeylem5  8910  tsksuc  9157  fsuppmapnn0fiublem  12099  fsuppmapnn0fiub  12100  invf  15184  sscres  15239  pgpssslw  16761  fislw  16772  frgpup1  16920  frgpup3lem  16922  dprdspan  17201  dprdz  17204  dprdf1o  17206  dprd2da  17218  ablfac1b  17248  lspsncmp  17889  lspsnne2  17891  lspsneq  17895  psrbaglesupp  18144  psrbaglesuppOLD  18145  psrbaglefi  18150  psrbaglefiOLD  18151  mplcoe5  18258  mplcoe2OLD  18260  mplbas2  18261  mplbas2OLD  18262  psgnghm2  18744  ofco2  19080  istps2OLD  19549  cncnpi  19906  hauscmplem  20033  iskgen2  20175  elqtop3  20330  qtoprest  20344  hmeores  20398  snfil  20491  uffixfr  20550  ustuqtop2  20871  tngngp2  21292  metnrmlem3  21491  volcn  22141  recnprss  22434  plyeq0  22734  chsupsn  26458  chlejb1i  26521  atsseq  27393  difneqnul  27543  measxun2  28354  measssd  28359  measiuns  28361  eulerpartlemb  28504  relexpnndm  29266  relexpdmg  29267  relexprng  29271  relexpfld  29274  relexpaddg  29278  funsseq  29416  ovoliunnfl  30261  voliunnfl  30263  volsupnfl  30264  opnbnd  30348  cldbnd  30349  fnemeet1  30389  heiborlem10  30521  smprngopr  30654  nacsfix  30849  dvconstbi  31443  icccncfext  31893  dvmptconst  31913  dvmptidg  31915  dvmulcncf  31925  dvdivcncf  31927  dirkercncflem2  32089  fourierdlem70  32162  fourierdlem71  32163  bnj1143  33992  bnj1322  34024  lshpcmp  34856  lsatcmp  34871  lsatcmp2  34872  lshpset2N  34987  paddasslem17  35703  pcl0bN  35790  pexmidALTN  35845  lcfrlem26  37438  lcfrlem36  37448  mapd0  37535  xptrrel  37935