Theorem eqimss 4022

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

Syntax hints:   → wi 4   = wceq 1533   ⊆ wss 3935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3942  df-ss 3951

This theorem is referenced by:  eqimss2  4023  sspss  4075  uneqin  4254  difn0  4323  ssdisj  4408  uneqdifeq  4437  pwpw0  4739  ssprsseq  4751  sssn  4752  snsspw  4768  pwsnALT  4824  unissint  4892  pwpwssunieq  5018  elpwuni  5019  disjeq2  5027  disjeq1  5030  pwne  5243  pwssun  5449  poeq2  5472  freq2  5520  seeq1  5521  seeq2  5522  frsn  5633  dmxpss  6022  xp11  6026  dmsnopss  6065  trsucss  6270  suc11  6288  iotassuni  6328  funeq  6369  fnresdm  6460  fssxp  6528  ffdm  6530  fcoi1  6546  fof  6584  dff1o2  6614  fvmptss  6774  fvmptss2  6787  funressn  6915  dff1o6  7026  suceloni  7522  tposeq  7888  tfrlem11  8018  oewordi  8211  oewordri  8212  dffi3  8889  cantnfle  9128  cantnflem2  9147  r1ord3g  9202  rankeq0b  9283  rankxplim3  9304  carddom2  9400  cflm  9666  cfsuc  9673  isf32lem2  9770  axdc3lem2  9867  ttukeylem5  9929  tsksuc  10178  fsuppmapnn0fiublem  13352  fsuppmapnn0fiub  13353  xptrrel  14334  relexpnndm  14394  relexpdmg  14395  relexprng  14399  relexpfld  14402  relexpaddg  14406  invf  17032  sscres  17087  pgpssslw  18733  fislw  18744  frgpup1  18895  frgpup3lem  18897  dprdspan  19143  dprdz  19146  dprdf1o  19148  dprd2da  19158  ablfac1b  19186  lspsncmp  19882  lspsnne2  19884  lspsneq  19888  psrbaglesupp  20142  psrbaglefi  20146  mplcoe5  20243  mplbas2  20245  psgnghm2  20719  ofco2  21054  toprntopon  21527  cncnpi  21880  hauscmplem  22008  iskgen2  22150  elqtop3  22305  qtoprest  22319  hmeores  22373  snfil  22466  uffixfr  22525  ustuqtop2  22845  tngngp2  23255  metnrmlem3  23463  volcn  24201  recnprss  24496  plyeq0  24795  uhgr3cyclex  27955  chsupsn  29184  chlejb1i  29247  atsseq  30118  disjeq1f  30317  ldgenpisys  31420  measxun2  31464  measssd  31469  measiuns  31471  pmeasmono  31577  eulerpartlemb  31621  bnj1143  32057  bnj1322  32089  funsseq  33006  opnbnd  33668  cldbnd  33669  fnemeet1  33709  bj-restuni  34382  bj-inexeqex  34440  bj-idreseq  34448  relowlpssretop  34639  pibt2  34692  ovoliunnfl  34928  voliunnfl  34930  volsupnfl  34931  heiborlem10  35092  smprngopr  35324  funALTVeq  35927  disjeq  35961  lshpcmp  36118  lsatcmp  36133  lsatcmp2  36134  lshpset2N  36249  paddasslem17  36966  pcl0bN  37053  pexmidALTN  37108  lcfrlem26  38698  lcfrlem36  38708  mapd0  38795  nacsfix  39302  cbviuneq12df  39999  relexp0a  40054  relexpaddss  40056  frege124d  40099  k0004lem3  40492  dvconstbi  40659  ssin0  41310  icccncfext  42163  dvmptconst  42192  dvmptidg  42194  dvmulcncf  42203  dvdivcncf  42205  dirkercncflem2  42383  fourierdlem70  42455  fourierdlem71  42456  hoicvr  42824  ovnsubaddlem1  42846  ovnhoi  42879  hspdifhsp  42892  0setrec  44800