Theorem eqimss 3396

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

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

Syntax hints:   -> wi 4   = wceq 1362   C_ wss 3316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-in 3323  df-ss 3330

This theorem is referenced by:  eqimss2  3397  sspss  3443  uneqin  3589  uneqdifeq  3755  pwpw0  4009  sssn  4019  eqsn  4022  snsspw  4032  pwsnALT  4074  unissint  4140  elpwuni  4246  disjeq2  4254  disjeq1  4257  pwne  4446  pwssun  4614  poeq2  4632  freq2  4678  seeq1  4679  seeq2  4680  trsucss  4791  suc11  4809  frsn  4896  dmxpss  5257  xp11  5261  dmsnopss  5299  iotassuni  5385  funeq  5425  fnresdm  5508  fssxp  5558  ffdm  5560  fcoi1  5573  fof  5608  dff1o2  5634  fvmptss  5770  fvmptss2  5781  funressn  5882  dff1o6  5969  suceloni  6413  tposeq  6736  tfrlem11  6833  oewordi  7018  oewordri  7019  dffi3  7669  cantnfle  7867  cantnflem2  7886  cantnfleOLD  7897  r1ord3g  7974  rankeq0b  8055  rankxplim3  8076  carddom2  8135  cflm  8407  cfsuc  8414  isf32lem2  8511  axdc3lem2  8608  ttukeylem5  8670  tsksuc  8917  invf  14689  sscres  14719  pgpssslw  16093  fislw  16104  frgpup1  16252  frgpup3lem  16254  dprdspan  16498  dprdz  16501  dprdf1o  16503  dprd2da  16515  ablfac1b  16545  lspsncmp  17119  lspsnne2  17121  lspsneq  17125  psrbaglesupp  17369  psrbaglesuppOLD  17370  psrbaglefi  17375  psrbaglefiOLD  17376  mplcoe2  17481  mplcoe2OLD  17482  mplbas2  17483  mplbas2OLD  17484  psgnghm2  17853  ofco2  18174  istps2OLD  18368  cncnpi  18724  hauscmplem  18851  iskgen2  18963  elqtop3  19118  qtoprest  19132  hmeores  19186  snfil  19279  uffixfr  19338  ustuqtop2  19659  tngngp2  20080  metnrmlem3  20279  volcn  20928  recnprss  21221  plyeq0  21564  chsupsn  24639  chlejb1i  24702  atsseq  25574  difneqnul  25722  measxun2  26478  measssd  26483  measiuns  26485  eulerpartlemb  26599  funsseq  27427  ovoliunnfl  28277  voliunnfl  28279  volsupnfl  28280  opnbnd  28364  cldbnd  28365  fnemeet1  28431  heiborlem10  28563  smprngopr  28696  nacsfix  28893  dvconstbi  29453  bnj1143  31486  bnj1322  31518  lshpcmp  32206  lsatcmp  32221  lsatcmp2  32222  lshpset2N  32337  paddasslem17  33053  pcl0bN  33140  pexmidALTN  33195  lcfrlem26  34786  lcfrlem36  34796  mapd0  34883