Theorem eqimss 3549

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

Syntax hints:   -> wi 4   = wceq 1374   C_ wss 3469

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-in 3476  df-ss 3483

This theorem is referenced by:  eqimss2  3550  sspss  3596  uneqin  3742  uneqdifeq  3908  pwpw0  4168  sssn  4178  eqsn  4181  snsspw  4191  pwsnALT  4233  unissint  4299  elpwuni  4406  disjeq2  4414  disjeq1  4417  pwne  4606  pwssun  4779  poeq2  4797  freq2  4843  seeq1  4844  seeq2  4845  trsucss  4956  suc11  4974  frsn  5062  dmxpss  5429  xp11  5433  dmsnopss  5471  iotassuni  5558  funeq  5598  fnresdm  5681  fssxp  5734  ffdm  5736  fcoi1  5750  fof  5786  dff1o2  5812  fvmptss  5949  fvmptss2  5960  funressn  6065  dff1o6  6160  suceloni  6619  tposeq  6947  tfrlem11  7047  oewordi  7230  oewordri  7231  dffi3  7880  cantnfle  8079  cantnflem2  8098  cantnfleOLD  8109  r1ord3g  8186  rankeq0b  8267  rankxplim3  8288  carddom2  8347  cflm  8619  cfsuc  8626  isf32lem2  8723  axdc3lem2  8820  ttukeylem5  8882  tsksuc  9129  fsuppmapnn0fiublem  12052  fsuppmapnn0fiub  12053  invf  15012  sscres  15042  pgpssslw  16423  fislw  16434  frgpup1  16582  frgpup3lem  16584  dprdspan  16857  dprdz  16860  dprdf1o  16862  dprd2da  16874  ablfac1b  16904  lspsncmp  17538  lspsnne2  17540  lspsneq  17544  psrbaglesupp  17781  psrbaglesuppOLD  17782  psrbaglefi  17787  psrbaglefiOLD  17788  mplcoe5  17895  mplcoe2OLD  17897  mplbas2  17898  mplbas2OLD  17899  psgnghm2  18377  ofco2  18713  istps2OLD  19182  cncnpi  19538  hauscmplem  19665  iskgen2  19777  elqtop3  19932  qtoprest  19946  hmeores  20000  snfil  20093  uffixfr  20152  ustuqtop2  20473  tngngp2  20894  metnrmlem3  21093  volcn  21743  recnprss  22036  plyeq0  22336  chsupsn  25857  chlejb1i  25920  atsseq  26792  difneqnul  26939  measxun2  27671  measssd  27676  measiuns  27678  eulerpartlemb  27797  funsseq  28626  ovoliunnfl  29484  voliunnfl  29486  volsupnfl  29487  opnbnd  29571  cldbnd  29572  fnemeet1  29638  heiborlem10  29770  smprngopr  29903  nacsfix  30099  dvconstbi  30658  icccncfext  31045  dvmptconst  31062  dvmptidg  31064  dvmulcncf  31074  dvdivcncf  31076  dirkercncflem2  31223  fourierdlem70  31296  fourierdlem71  31297  bnj1143  32803  bnj1322  32835  lshpcmp  33660  lsatcmp  33675  lsatcmp2  33676  lshpset2N  33791  paddasslem17  34507  pcl0bN  34594  pexmidALTN  34649  lcfrlem26  36240  lcfrlem36  36250  mapd0  36337  xptrrel  36660