Theorem eqimss 3403

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

Syntax hints:   -> wi 4   = wceq 1369   C_ wss 3323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3330  df-ss 3337

This theorem is referenced by:  eqimss2  3404  sspss  3450  uneqin  3596  uneqdifeq  3762  pwpw0  4016  sssn  4026  eqsn  4029  snsspw  4039  pwsnALT  4081  unissint  4147  elpwuni  4253  disjeq2  4261  disjeq1  4264  pwne  4453  pwssun  4622  poeq2  4640  freq2  4686  seeq1  4687  seeq2  4688  trsucss  4799  suc11  4817  frsn  4904  dmxpss  5264  xp11  5268  dmsnopss  5306  iotassuni  5392  funeq  5432  fnresdm  5515  fssxp  5565  ffdm  5567  fcoi1  5580  fof  5615  dff1o2  5641  fvmptss  5777  fvmptss2  5788  funressn  5890  dff1o6  5977  suceloni  6419  tposeq  6742  tfrlem11  6839  oewordi  7022  oewordri  7023  dffi3  7673  cantnfle  7871  cantnflem2  7890  cantnfleOLD  7901  r1ord3g  7978  rankeq0b  8059  rankxplim3  8080  carddom2  8139  cflm  8411  cfsuc  8418  isf32lem2  8515  axdc3lem2  8612  ttukeylem5  8674  tsksuc  8921  invf  14698  sscres  14728  pgpssslw  16104  fislw  16115  frgpup1  16263  frgpup3lem  16265  dprdspan  16514  dprdz  16517  dprdf1o  16519  dprd2da  16531  ablfac1b  16561  lspsncmp  17177  lspsnne2  17179  lspsneq  17183  psrbaglesupp  17415  psrbaglesuppOLD  17416  psrbaglefi  17421  psrbaglefiOLD  17422  mplcoe5  17528  mplcoe2OLD  17530  mplbas2  17531  mplbas2OLD  17532  psgnghm2  17991  ofco2  18312  istps2OLD  18506  cncnpi  18862  hauscmplem  18989  iskgen2  19101  elqtop3  19256  qtoprest  19270  hmeores  19324  snfil  19417  uffixfr  19476  ustuqtop2  19797  tngngp2  20218  metnrmlem3  20417  volcn  21066  recnprss  21359  plyeq0  21659  chsupsn  24784  chlejb1i  24847  atsseq  25719  difneqnul  25866  measxun2  26593  measssd  26598  measiuns  26600  eulerpartlemb  26720  funsseq  27549  ovoliunnfl  28404  voliunnfl  28406  volsupnfl  28407  opnbnd  28491  cldbnd  28492  fnemeet1  28558  heiborlem10  28690  smprngopr  28823  nacsfix  29019  dvconstbi  29579  fsuppmapnn0fiublem  30767  fsuppmapnn0fiub  30768  bnj1143  31713  bnj1322  31745  lshpcmp  32526  lsatcmp  32541  lsatcmp2  32542  lshpset2N  32657  paddasslem17  33373  pcl0bN  33460  pexmidALTN  33515  lcfrlem26  35106  lcfrlem36  35116  mapd0  35203