Theorem eqimss 3516

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

Syntax hints:   -> wi 4   = wceq 1437   C_ wss 3436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-in 3443  df-ss 3450

This theorem is referenced by:  eqimss2  3517  sspss  3564  uneqin  3724  difn0  3854  uneqdifeq  3886  pwpw0  4148  sssn  4158  eqsn  4161  snsspw  4171  pwsnALT  4214  unissint  4280  elpwuni  4390  disjeq2  4398  disjeq1  4401  pwne  4590  pwssun  4759  poeq2  4778  freq2  4824  seeq1  4825  seeq2  4826  frsn  4924  dmxpss  5287  xp11  5291  dmsnopss  5327  trsucss  5527  suc11  5545  iotassuni  5581  funeq  5620  fnresdm  5703  fssxp  5758  ffdm  5760  fcoi1  5774  fof  5810  dff1o2  5836  fvmptss  5974  fvmptss2  5985  funressn  6092  dff1o6  6189  suceloni  6654  tposeq  6986  tfrlem11  7117  oewordi  7303  oewordri  7304  dffi3  7954  cantnfle  8184  cantnflem2  8203  r1ord3g  8258  rankeq0b  8339  rankxplim3  8360  carddom2  8419  cflm  8687  cfsuc  8694  isf32lem2  8791  axdc3lem2  8888  ttukeylem5  8950  tsksuc  9194  fsuppmapnn0fiublem  12208  fsuppmapnn0fiub  12209  xptrrel  13044  relexpnndm  13104  relexpdmg  13105  relexprng  13109  relexpfld  13112  relexpaddg  13116  invf  15672  sscres  15727  pgpssslw  17265  fislw  17276  frgpup1  17424  frgpup3lem  17426  dprdspan  17659  dprdz  17662  dprdf1o  17664  dprd2da  17674  ablfac1b  17702  lspsncmp  18338  lspsnne2  18340  lspsneq  18344  psrbaglesupp  18591  psrbaglefi  18595  mplcoe5  18691  mplbas2  18693  psgnghm2  19147  ofco2  19474  cncnpi  20292  hauscmplem  20419  iskgen2  20561  elqtop3  20716  qtoprest  20730  hmeores  20784  snfil  20877  uffixfr  20936  ustuqtop2  21255  tngngp2  21658  metnrmlem3  21876  metnrmlem3OLD  21891  volcn  22562  recnprss  22857  plyeq0  23163  chsupsn  27064  chlejb1i  27127  atsseq  27998  disjeq1f  28186  ldgenpisys  28996  measxun2  29040  measssd  29045  measiuns  29047  pmeasmono  29165  eulerpartlemb  29209  bnj1143  29610  bnj1322  29642  funsseq  30416  opnbnd  30986  cldbnd  30987  fnemeet1  31027  relowlpssretop  31731  ovoliunnfl  31946  voliunnfl  31948  volsupnfl  31949  heiborlem10  32116  smprngopr  32249  lshpcmp  32523  lsatcmp  32538  lsatcmp2  32539  lshpset2N  32654  paddasslem17  33370  pcl0bN  33457  pexmidALTN  33512  lcfrlem26  35105  lcfrlem36  35115  mapd0  35202  nacsfix  35523  cbviuneq12df  36223  relexp0a  36278  relexpaddss  36280  frege124d  36323  dvconstbi  36653  ssin0  37368  icccncfext  37705  dvmptconst  37725  dvmptidg  37727  dvmulcncf  37737  dvdivcncf  37739  dirkercncflem2  37906  fourierdlem70  37980  fourierdlem71  37981  hoicvr  38274  ovnsubaddlem1  38296  ovnhoi  38329  ssprsseq  38868  structvtxvallem  38952