Theorem eqimss 3971

Description: Equality implies the subclass relation. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)

Assertion

Ref	Expression
eqimss	⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)

Proof of Theorem eqimss

Step	Hyp	Ref	Expression
1		eqss 3930	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2	1	simplbi 501	1 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4   = wceq 1538   ⊆ wss 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  eqimss2  3972  sspss  4027  uneqin  4205  difn0  4278  ssdisj  4367  uneqdifeq  4396  pweq  4513  pwpw0  4706  ssprsseq  4718  sssn  4719  snsspw  4735  pwsnOLD  4793  unieq  4811  unissint  4862  pwpwssunieq  4989  elpwuni  4990  disjeq2  4999  disjeq1  5002  pwne  5216  pwssun  5421  poeq2  5442  freq2  5490  seeq1  5491  seeq2  5492  frsn  5603  dmxpss  5995  xp11  5999  dmsnopss  6038  trsucss  6244  suc11  6262  iotassuni  6303  funeq  6344  fnresdm  6438  fssxp  6508  ffdm  6510  fcoi1  6526  fof  6565  dff1o2  6595  fvmptss  6757  fvmptss2  6770  funressn  6898  dff1o6  7010  suceloni  7508  tposeq  7877  tfrlem11  8007  oewordi  8200  oewordri  8201  dffi3  8879  cantnfle  9118  cantnflem2  9137  r1ord3g  9192  rankeq0b  9273  rankxplim3  9294  carddom2  9390  cflm  9661  cfsuc  9668  isf32lem2  9765  axdc3lem2  9862  ttukeylem5  9924  tsksuc  10173  fsuppmapnn0fiublem  13353  fsuppmapnn0fiub  13354  xptrrel  14331  relexpnndm  14392  relexpdmg  14393  relexprng  14397  relexpfld  14400  relexpaddg  14404  invf  17030  sscres  17085  pgpssslw  18731  fislw  18742  frgpup1  18893  frgpup3lem  18895  dprdspan  19142  dprdz  19145  dprdf1o  19147  dprd2da  19157  ablfac1b  19185  lspsncmp  19881  lspsnne2  19883  lspsneq  19887  psgnghm2  20270  psrbaglesupp  20606  psrbaglefi  20610  mplcoe5  20708  mplbas2  20710  ofco2  21056  toprntopon  21530  cncnpi  21883  hauscmplem  22011  iskgen2  22153  elqtop3  22308  qtoprest  22322  hmeores  22376  snfil  22469  uffixfr  22528  ustuqtop2  22848  tngngp2  23258  metnrmlem3  23466  volcn  24210  recnprss  24507  plyeq0  24808  uhgr3cyclex  27967  chsupsn  29196  chlejb1i  29259  atsseq  30130  disjeq1f  30336  ldgenpisys  31535  measxun2  31579  measssd  31584  measiuns  31586  pmeasmono  31692  eulerpartlemb  31736  bnj1143  32172  bnj1322  32204  funsseq  33124  opnbnd  33786  cldbnd  33787  fnemeet1  33827  bj-restuni  34512  bj-inexeqex  34569  bj-idreseq  34577  relowlpssretop  34781  pibt2  34834  ovoliunnfl  35099  voliunnfl  35101  volsupnfl  35102  heiborlem10  35258  smprngopr  35490  funALTVeq  36093  disjeq  36127  lshpcmp  36284  lsatcmp  36299  lsatcmp2  36300  lshpset2N  36415  paddasslem17  37132  pcl0bN  37219  pexmidALTN  37274  lcfrlem26  38864  lcfrlem36  38874  mapd0  38961  nacsfix  39653  cbviuneq12df  40362  relexp0a  40417  relexpaddss  40419  frege124d  40462  k0004lem3  40852  dvconstbi  41038  ssin0  41689  icccncfext  42529  dvmptconst  42557  dvmptidg  42559  dvmulcncf  42567  dvdivcncf  42569  dirkercncflem2  42746  fourierdlem70  42818  fourierdlem71  42819  hoicvr  43187  ovnsubaddlem1  43209  ovnhoi  43242  hspdifhsp  43255  0setrec  45233