Theorem eqimss 3496

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

Syntax hints:   -> wi 4   = wceq 1455   C_ wss 3416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-in 3423  df-ss 3430

This theorem is referenced by:  eqimss2  3497  sspss  3544  uneqin  3706  difn0  3836  uneqdifeq  3868  pwpw0  4133  sssn  4143  eqsn  4146  snsspw  4156  pwsnALT  4207  unissint  4273  elpwuni  4385  disjeq2  4393  disjeq1  4396  pwne  4586  pwssun  4762  poeq2  4781  freq2  4827  seeq1  4828  seeq2  4829  frsn  4927  dmxpss  5290  xp11  5294  dmsnopss  5331  trsucss  5531  suc11  5549  iotassuni  5585  funeq  5624  fnresdm  5711  fssxp  5768  ffdm  5770  fcoi1  5784  fof  5820  dff1o2  5846  fvmptss  5986  fvmptss2  5997  funressn  6106  dff1o6  6204  suceloni  6672  tposeq  7006  tfrlem11  7137  oewordi  7323  oewordri  7324  dffi3  7976  cantnfle  8207  cantnflem2  8226  r1ord3g  8281  rankeq0b  8362  rankxplim3  8383  carddom2  8442  cflm  8711  cfsuc  8718  isf32lem2  8815  axdc3lem2  8912  ttukeylem5  8974  tsksuc  9218  fsuppmapnn0fiublem  12240  fsuppmapnn0fiub  12241  xptrrel  13099  relexpnndm  13159  relexpdmg  13160  relexprng  13164  relexpfld  13167  relexpaddg  13171  invf  15728  sscres  15783  pgpssslw  17321  fislw  17332  frgpup1  17480  frgpup3lem  17482  dprdspan  17715  dprdz  17718  dprdf1o  17720  dprd2da  17730  ablfac1b  17758  lspsncmp  18394  lspsnne2  18396  lspsneq  18400  psrbaglesupp  18647  psrbaglefi  18651  mplcoe5  18747  mplbas2  18749  psgnghm2  19204  ofco2  19531  cncnpi  20349  hauscmplem  20476  iskgen2  20618  elqtop3  20773  qtoprest  20787  hmeores  20841  snfil  20934  uffixfr  20993  ustuqtop2  21312  tngngp2  21715  metnrmlem3  21933  metnrmlem3OLD  21948  volcn  22620  recnprss  22915  plyeq0  23221  chsupsn  27122  chlejb1i  27185  atsseq  28056  disjeq1f  28238  ldgenpisys  29039  measxun2  29083  measssd  29088  measiuns  29090  pmeasmono  29207  eulerpartlemb  29251  bnj1143  29652  bnj1322  29684  funsseq  30459  opnbnd  31031  cldbnd  31032  fnemeet1  31072  relowlpssretop  31813  ovoliunnfl  32028  voliunnfl  32030  volsupnfl  32031  heiborlem10  32198  smprngopr  32331  lshpcmp  32600  lsatcmp  32615  lsatcmp2  32616  lshpset2N  32731  paddasslem17  33447  pcl0bN  33534  pexmidALTN  33589  lcfrlem26  35182  lcfrlem36  35192  mapd0  35279  nacsfix  35600  cbviuneq12df  36299  relexp0a  36354  relexpaddss  36356  frege124d  36399  dvconstbi  36728  ssin0  37434  icccncfext  37851  dvmptconst  37871  dvmptidg  37873  dvmulcncf  37883  dvdivcncf  37885  dirkercncflem2  38067  fourierdlem70  38141  fourierdlem71  38142  hoicvr  38477  ovnsubaddlem1  38499  ovnhoi  38532  hspdifhsp  38545  ssprsseq  39139  structvtxvallem  39264  uhgr3cyclex  40019