MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqimss Structured version   Visualization version   GIF version

Theorem eqimss 3998
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
StepHypRef Expression
1 eqss 3957 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
21simplbi 501 1 (𝐴 = 𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wss 3908
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 2116  ax-9 2124  ax-ext 2794
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-v 3471  df-in 3915  df-ss 3925
This theorem is referenced by:  eqimss2  3999  sspss  4051  uneqin  4229  difn0  4296  ssdisj  4381  uneqdifeq  4410  pweq  4527  pwpw0  4719  ssprsseq  4731  sssn  4732  snsspw  4748  pwsnOLD  4806  unieq  4824  unissint  4875  pwpwssunieq  5001  elpwuni  5002  disjeq2  5011  disjeq1  5014  pwne  5228  pwssun  5433  poeq2  5455  freq2  5503  seeq1  5504  seeq2  5505  frsn  5616  dmxpss  6006  xp11  6010  dmsnopss  6049  trsucss  6254  suc11  6272  iotassuni  6313  funeq  6354  fnresdm  6446  fssxp  6515  ffdm  6517  fcoi1  6533  fof  6572  dff1o2  6602  fvmptss  6762  fvmptss2  6775  funressn  6903  dff1o6  7015  suceloni  7513  tposeq  7881  tfrlem11  8011  oewordi  8204  oewordri  8205  dffi3  8883  cantnfle  9122  cantnflem2  9141  r1ord3g  9196  rankeq0b  9277  rankxplim3  9298  carddom2  9394  cflm  9661  cfsuc  9668  isf32lem2  9765  axdc3lem2  9862  ttukeylem5  9924  tsksuc  10173  fsuppmapnn0fiublem  13353  fsuppmapnn0fiub  13354  xptrrel  14331  relexpnndm  14391  relexpdmg  14392  relexprng  14396  relexpfld  14399  relexpaddg  14403  invf  17029  sscres  17084  pgpssslw  18730  fislw  18741  frgpup1  18892  frgpup3lem  18894  dprdspan  19140  dprdz  19143  dprdf1o  19145  dprd2da  19155  ablfac1b  19183  lspsncmp  19879  lspsnne2  19881  lspsneq  19885  psgnghm2  20268  psrbaglesupp  20604  psrbaglefi  20608  mplcoe5  20706  mplbas2  20708  ofco2  21054  toprntopon  21528  cncnpi  21881  hauscmplem  22009  iskgen2  22151  elqtop3  22306  qtoprest  22320  hmeores  22374  snfil  22467  uffixfr  22526  ustuqtop2  22846  tngngp2  23256  metnrmlem3  23464  volcn  24208  recnprss  24505  plyeq0  24806  uhgr3cyclex  27965  chsupsn  29194  chlejb1i  29257  atsseq  30128  disjeq1f  30331  ldgenpisys  31499  measxun2  31543  measssd  31548  measiuns  31550  pmeasmono  31656  eulerpartlemb  31700  bnj1143  32136  bnj1322  32168  funsseq  33085  opnbnd  33747  cldbnd  33748  fnemeet1  33788  bj-restuni  34473  bj-inexeqex  34530  bj-idreseq  34538  relowlpssretop  34742  pibt2  34795  ovoliunnfl  35057  voliunnfl  35059  volsupnfl  35060  heiborlem10  35216  smprngopr  35448  funALTVeq  36051  disjeq  36085  lshpcmp  36242  lsatcmp  36257  lsatcmp2  36258  lshpset2N  36373  paddasslem17  37090  pcl0bN  37177  pexmidALTN  37232  lcfrlem26  38822  lcfrlem36  38832  mapd0  38919  nacsfix  39583  cbviuneq12df  40292  relexp0a  40347  relexpaddss  40349  frege124d  40392  k0004lem3  40785  dvconstbi  40972  ssin0  41623  icccncfext  42468  dvmptconst  42496  dvmptidg  42498  dvmulcncf  42506  dvdivcncf  42508  dirkercncflem2  42685  fourierdlem70  42757  fourierdlem71  42758  hoicvr  43126  ovnsubaddlem1  43148  ovnhoi  43181  hspdifhsp  43194  0setrec  45172
  Copyright terms: Public domain W3C validator