Theorem eqimss 3657

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

Syntax hints:   -> wi 4   = wceq 1483   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  eqimss2  3658  sspss  3706  uneqin  3878  difn0  3943  ssdisj  4026  uneqdifeq  4057  uneqdifeqOLD  4058  pwpw0  4344  ssprsseq  4357  sssn  4358  eqsnOLD  4362  snsspw  4375  pwsnALT  4429  unissint  4501  pwpwssunieq  4615  elpwuni  4616  disjeq2  4624  disjeq1  4627  pwne  4831  pwssun  5020  poeq2  5039  freq2  5085  seeq1  5086  seeq2  5087  frsn  5189  dmxpss  5565  xp11  5569  dmsnopss  5607  trsucss  5811  suc11  5831  iotassuni  5867  funeq  5908  fnresdm  6000  fssxp  6060  ffdm  6062  fcoi1  6078  fof  6115  dff1o2  6142  fvmptss  6292  fvmptss2  6304  funressn  6426  dff1o6  6531  suceloni  7013  tposeq  7354  tfrlem11  7484  oewordi  7671  oewordri  7672  dffi3  8337  cantnfle  8568  cantnflem2  8587  r1ord3g  8642  rankeq0b  8723  rankxplim3  8744  carddom2  8803  cflm  9072  cfsuc  9079  isf32lem2  9176  axdc3lem2  9273  ttukeylem5  9335  tsksuc  9584  fsuppmapnn0fiublem  12789  fsuppmapnn0fiub  12790  fsuppmapnn0fiubOLD  12791  xptrrel  13719  relexpnndm  13781  relexpdmg  13782  relexprng  13786  relexpfld  13789  relexpaddg  13793  invf  16428  sscres  16483  pgpssslw  18029  fislw  18040  frgpup1  18188  frgpup3lem  18190  dprdspan  18426  dprdz  18429  dprdf1o  18431  dprd2da  18441  ablfac1b  18469  lspsncmp  19116  lspsnne2  19118  lspsneq  19122  psrbaglesupp  19368  psrbaglefi  19372  mplcoe5  19468  mplbas2  19470  psgnghm2  19927  ofco2  20257  toprntopon  20729  cncnpi  21082  hauscmplem  21209  iskgen2  21351  elqtop3  21506  qtoprest  21520  hmeores  21574  snfil  21668  uffixfr  21727  ustuqtop2  22046  tngngp2  22456  metnrmlem3  22664  volcn  23374  recnprss  23668  plyeq0  23967  uhgr3cyclex  27042  chsupsn  28272  chlejb1i  28335  atsseq  29206  disjeq1f  29387  ldgenpisys  30229  measxun2  30273  measssd  30278  measiuns  30280  pmeasmono  30386  eulerpartlemb  30430  bnj1143  30861  bnj1322  30893  funsseq  31666  opnbnd  32320  cldbnd  32321  fnemeet1  32361  bj-restuni  33050  relowlpssretop  33212  ovoliunnfl  33451  voliunnfl  33453  volsupnfl  33454  heiborlem10  33619  smprngopr  33851  lshpcmp  34275  lsatcmp  34290  lsatcmp2  34291  lshpset2N  34406  paddasslem17  35122  pcl0bN  35209  pexmidALTN  35264  lcfrlem26  36857  lcfrlem36  36867  mapd0  36954  nacsfix  37275  cbviuneq12df  37953  relexp0a  38008  relexpaddss  38010  frege124d  38053  k0004lem3  38447  dvconstbi  38533  ssin0  39223  icccncfext  40100  dvmptconst  40129  dvmptidg  40131  dvmulcncf  40140  dvdivcncf  40142  dirkercncflem2  40321  fourierdlem70  40393  fourierdlem71  40394  hoicvr  40762  ovnsubaddlem1  40784  ovnhoi  40817  hspdifhsp  40830  0setrec  42447