Theorem eqimss 3909

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 3869	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2	1	simplbi 490	1 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4   = wceq 1507   ⊆ wss 3825

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2754  df-cleq 2765  df-clel 2840  df-in 3832  df-ss 3839

This theorem is referenced by:  eqimss2  3910  sspss  3962  uneqin  4137  difn0  4205  ssdisj  4286  uneqdifeq  4315  pwpw0  4614  ssprsseq  4626  sssn  4627  snsspw  4643  pwsnALT  4699  unissint  4767  pwpwssunieq  4886  elpwuni  4887  disjeq2  4895  disjeq1  4898  pwne  5101  pwssun  5301  poeq2  5323  freq2  5371  seeq1  5372  seeq2  5373  frsn  5482  dmxpss  5862  xp11  5866  dmsnopss  5904  trsucss  6108  suc11  6126  iotassuni  6162  funeq  6202  fnresdm  6293  fssxp  6357  ffdm  6359  fcoi1  6375  fof  6413  dff1o2  6443  fvmptss  6600  fvmptss2  6613  funressn  6738  dff1o6  6851  suceloni  7338  tposeq  7690  tfrlem11  7821  oewordi  8010  oewordri  8011  dffi3  8682  cantnfle  8920  cantnflem2  8939  r1ord3g  8994  rankeq0b  9075  rankxplim3  9096  carddom2  9192  cflm  9462  cfsuc  9469  isf32lem2  9566  axdc3lem2  9663  ttukeylem5  9725  tsksuc  9974  fsuppmapnn0fiublem  13166  fsuppmapnn0fiub  13167  xptrrel  14191  relexpnndm  14251  relexpdmg  14252  relexprng  14256  relexpfld  14259  relexpaddg  14263  invf  16886  sscres  16941  pgpssslw  18490  fislw  18501  frgpup1  18651  frgpup3lem  18653  dprdspan  18889  dprdz  18892  dprdf1o  18894  dprd2da  18904  ablfac1b  18932  lspsncmp  19600  lspsnne2  19602  lspsneq  19606  psrbaglesupp  19852  psrbaglefi  19856  mplcoe5  19952  mplbas2  19954  psgnghm2  20417  ofco2  20754  toprntopon  21227  cncnpi  21580  hauscmplem  21708  iskgen2  21850  elqtop3  22005  qtoprest  22019  hmeores  22073  snfil  22166  uffixfr  22225  ustuqtop2  22544  tngngp2  22954  metnrmlem3  23162  volcn  23900  recnprss  24195  plyeq0  24494  uhgr3cyclex  27701  chsupsn  28961  chlejb1i  29024  atsseq  29895  disjeq1f  30080  ldgenpisys  31027  measxun2  31071  measssd  31076  measiuns  31078  pmeasmono  31184  eulerpartlemb  31228  bnj1143  31671  bnj1322  31703  funsseq  32471  opnbnd  33134  cldbnd  33135  fnemeet1  33175  bj-restuni  33833  relowlpssretop  34022  pibt2  34074  ovoliunnfl  34323  voliunnfl  34325  volsupnfl  34326  heiborlem10  34488  smprngopr  34720  funALTVeq  35326  disjeq  35360  lshpcmp  35517  lsatcmp  35532  lsatcmp2  35533  lshpset2N  35648  paddasslem17  36365  pcl0bN  36452  pexmidALTN  36507  lcfrlem26  38097  lcfrlem36  38107  mapd0  38194  nacsfix  38649  cbviuneq12df  39314  relexp0a  39369  relexpaddss  39371  frege124d  39414  k0004lem3  39807  dvconstbi  40026  ssin0  40681  icccncfext  41546  dvmptconst  41575  dvmptidg  41577  dvmulcncf  41586  dvdivcncf  41588  dirkercncflem2  41766  fourierdlem70  41838  fourierdlem71  41839  hoicvr  42207  ovnsubaddlem1  42229  ovnhoi  42262  hspdifhsp  42275  0setrec  44113