Theorem eqimss 3506

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

Syntax hints:   -> wi 4   = wceq 1370   C_ wss 3426

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-in 3433  df-ss 3440

This theorem is referenced by:  eqimss2  3507  sspss  3553  uneqin  3699  uneqdifeq  3865  pwpw0  4119  sssn  4129  eqsn  4132  snsspw  4142  pwsnALT  4184  unissint  4250  elpwuni  4356  disjeq2  4364  disjeq1  4367  pwne  4556  pwssun  4725  poeq2  4743  freq2  4789  seeq1  4790  seeq2  4791  trsucss  4902  suc11  4920  frsn  5007  dmxpss  5367  xp11  5371  dmsnopss  5409  iotassuni  5495  funeq  5535  fnresdm  5618  fssxp  5668  ffdm  5670  fcoi1  5683  fof  5718  dff1o2  5744  fvmptss  5881  fvmptss2  5892  funressn  5994  dff1o6  6081  suceloni  6524  tposeq  6847  tfrlem11  6947  oewordi  7130  oewordri  7131  dffi3  7782  cantnfle  7980  cantnflem2  7999  cantnfleOLD  8010  r1ord3g  8087  rankeq0b  8168  rankxplim3  8189  carddom2  8248  cflm  8520  cfsuc  8527  isf32lem2  8624  axdc3lem2  8721  ttukeylem5  8783  tsksuc  9030  invf  14808  sscres  14838  pgpssslw  16217  fislw  16228  frgpup1  16376  frgpup3lem  16378  dprdspan  16629  dprdz  16632  dprdf1o  16634  dprd2da  16646  ablfac1b  16676  lspsncmp  17303  lspsnne2  17305  lspsneq  17309  psrbaglesupp  17541  psrbaglesuppOLD  17542  psrbaglefi  17547  psrbaglefiOLD  17548  mplcoe5  17655  mplcoe2OLD  17657  mplbas2  17658  mplbas2OLD  17659  psgnghm2  18120  ofco2  18443  istps2OLD  18642  cncnpi  18998  hauscmplem  19125  iskgen2  19237  elqtop3  19392  qtoprest  19406  hmeores  19460  snfil  19553  uffixfr  19612  ustuqtop2  19933  tngngp2  20354  metnrmlem3  20553  volcn  21202  recnprss  21495  plyeq0  21795  chsupsn  24951  chlejb1i  25014  atsseq  25886  difneqnul  26033  measxun2  26758  measssd  26763  measiuns  26765  eulerpartlemb  26885  funsseq  27714  ovoliunnfl  28571  voliunnfl  28573  volsupnfl  28574  opnbnd  28658  cldbnd  28659  fnemeet1  28725  heiborlem10  28857  smprngopr  28990  nacsfix  29186  dvconstbi  29746  fsuppmapnn0fiublem  30936  fsuppmapnn0fiub  30937  bnj1143  32084  bnj1322  32116  lshpcmp  32939  lsatcmp  32954  lsatcmp2  32955  lshpset2N  33070  paddasslem17  33786  pcl0bN  33873  pexmidALTN  33928  lcfrlem26  35519  lcfrlem36  35529  mapd0  35616