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

Theorem eqimss 3620
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 3583 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
21simplbi 475 1 (𝐴 = 𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475  wss 3540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554
This theorem is referenced by:  eqimss2  3621  sspss  3668  uneqin  3837  difn0  3897  ssdisj  3978  uneqdifeq  4009  uneqdifeqOLD  4010  pwpw0  4284  ssprsseq  4297  sssn  4298  eqsnOLD  4302  snsspw  4315  pwsnALT  4367  unissint  4436  elpwuni  4549  disjeq2  4557  disjeq1  4560  pwne  4757  pwssun  4944  poeq2  4963  freq2  5009  seeq1  5010  seeq2  5011  frsn  5112  dmxpss  5484  xp11  5488  dmsnopss  5525  trsucss  5728  suc11  5748  iotassuni  5784  funeq  5823  fnresdm  5914  fssxp  5973  ffdm  5975  fcoi1  5991  fof  6028  dff1o2  6055  fvmptss  6201  fvmptss2  6212  funressn  6331  dff1o6  6431  suceloni  6905  tposeq  7241  tfrlem11  7371  oewordi  7558  oewordri  7559  dffi3  8220  cantnfle  8451  cantnflem2  8470  r1ord3g  8525  rankeq0b  8606  rankxplim3  8627  carddom2  8686  cflm  8955  cfsuc  8962  isf32lem2  9059  axdc3lem2  9156  ttukeylem5  9218  tsksuc  9463  fsuppmapnn0fiublem  12651  fsuppmapnn0fiub  12652  fsuppmapnn0fiubOLD  12653  xptrrel  13567  relexpnndm  13629  relexpdmg  13630  relexprng  13634  relexpfld  13637  relexpaddg  13641  invf  16251  sscres  16306  pgpssslw  17852  fislw  17863  frgpup1  18011  frgpup3lem  18013  dprdspan  18249  dprdz  18252  dprdf1o  18254  dprd2da  18264  ablfac1b  18292  lspsncmp  18937  lspsnne2  18939  lspsneq  18943  psrbaglesupp  19189  psrbaglefi  19193  mplcoe5  19289  mplbas2  19291  psgnghm2  19746  ofco2  20076  cncnpi  20892  hauscmplem  21019  iskgen2  21161  elqtop3  21316  qtoprest  21330  hmeores  21384  snfil  21478  uffixfr  21537  ustuqtop2  21856  tngngp2  22266  metnrmlem3  22472  volcn  23180  recnprss  23474  plyeq0  23771  structvtxvallem  25697  chsupsn  27656  chlejb1i  27719  atsseq  28590  disjeq1f  28769  ldgenpisys  29556  measxun2  29600  measssd  29605  measiuns  29607  pmeasmono  29713  eulerpartlemb  29757  bnj1143  30115  bnj1322  30147  funsseq  30912  opnbnd  31490  cldbnd  31491  fnemeet1  31531  bj-restuni  32231  bj-sspwpweq  32240  bj-toprntopon  32244  relowlpssretop  32388  ovoliunnfl  32621  voliunnfl  32623  volsupnfl  32624  heiborlem10  32789  smprngopr  33021  lshpcmp  33293  lsatcmp  33308  lsatcmp2  33309  lshpset2N  33424  paddasslem17  34140  pcl0bN  34227  pexmidALTN  34282  lcfrlem26  35875  lcfrlem36  35885  mapd0  35972  nacsfix  36293  cbviuneq12df  36972  relexp0a  37027  relexpaddss  37029  frege124d  37072  k0004lem3  37467  dvconstbi  37555  ssin0  38248  icccncfext  38773  dvmptconst  38803  dvmptidg  38805  dvmulcncf  38815  dvdivcncf  38817  dirkercncflem2  38997  fourierdlem70  39069  fourierdlem71  39070  hoicvr  39438  ovnsubaddlem1  39460  ovnhoi  39493  hspdifhsp  39506  uhgr3cyclex  41349  0setrec  42246
  Copyright terms: Public domain W3C validator