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

Theorem eqimss 3861
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 3820 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
21simplbi 487 1 (𝐴 = 𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  wss 3776
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-ext 2791
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2800  df-cleq 2806  df-clel 2809  df-in 3783  df-ss 3790
This theorem is referenced by:  eqimss2  3862  sspss  3911  uneqin  4087  difn0  4151  ssdisj  4231  uneqdifeq  4260  pwpw0  4541  ssprsseq  4553  sssn  4554  snsspw  4570  pwsnALT  4630  unissint  4700  pwpwssunieq  4814  elpwuni  4815  disjeq2  4823  disjeq1  4826  pwne  5030  pwssun  5222  poeq2  5243  freq2  5289  seeq1  5290  seeq2  5291  frsn  5398  dmxpss  5783  xp11  5787  dmsnopss  5826  trsucss  6029  suc11  6047  iotassuni  6083  funeq  6124  fnresdm  6214  fssxp  6278  ffdm  6280  fcoi1  6296  fof  6334  dff1o2  6361  fvmptss  6516  fvmptss2  6528  funressn  6653  dff1o6  6758  suceloni  7246  tposeq  7592  tfrlem11  7723  oewordi  7911  oewordri  7912  dffi3  8579  cantnfle  8818  cantnflem2  8837  r1ord3g  8892  rankeq0b  8973  rankxplim3  8994  carddom2  9089  cflm  9360  cfsuc  9367  isf32lem2  9464  axdc3lem2  9561  ttukeylem5  9623  tsksuc  9872  fsuppmapnn0fiublem  13016  fsuppmapnn0fiub  13017  xptrrel  13947  relexpnndm  14007  relexpdmg  14008  relexprng  14012  relexpfld  14015  relexpaddg  14019  invf  16635  sscres  16690  pgpssslw  18233  fislw  18244  frgpup1  18392  frgpup3lem  18394  dprdspan  18631  dprdz  18634  dprdf1o  18636  dprd2da  18646  ablfac1b  18674  lspsncmp  19326  lspsnne2  19328  lspsneq  19332  psrbaglesupp  19580  psrbaglefi  19584  mplcoe5  19680  mplbas2  19682  psgnghm2  20137  ofco2  20472  toprntopon  20947  cncnpi  21300  hauscmplem  21427  iskgen2  21569  elqtop3  21724  qtoprest  21738  hmeores  21792  snfil  21885  uffixfr  21944  ustuqtop2  22263  tngngp2  22673  metnrmlem3  22881  volcn  23593  recnprss  23888  plyeq0  24187  uhgr3cyclex  27361  chsupsn  28606  chlejb1i  28669  atsseq  29540  disjeq1f  29718  ldgenpisys  30560  measxun2  30604  measssd  30609  measiuns  30611  pmeasmono  30717  eulerpartlemb  30761  bnj1143  31189  bnj1322  31221  funsseq  31993  opnbnd  32646  cldbnd  32647  fnemeet1  32687  bj-restuni  33363  relowlpssretop  33530  ovoliunnfl  33766  voliunnfl  33768  volsupnfl  33769  heiborlem10  33932  smprngopr  34164  lshpcmp  34770  lsatcmp  34785  lsatcmp2  34786  lshpset2N  34901  paddasslem17  35618  pcl0bN  35705  pexmidALTN  35760  lcfrlem26  37350  lcfrlem36  37360  mapd0  37447  nacsfix  37778  cbviuneq12df  38454  relexp0a  38509  relexpaddss  38511  frege124d  38554  k0004lem3  38948  dvconstbi  39034  ssin0  39717  icccncfext  40581  dvmptconst  40610  dvmptidg  40612  dvmulcncf  40621  dvdivcncf  40623  dirkercncflem2  40801  fourierdlem70  40873  fourierdlem71  40874  hoicvr  41245  ovnsubaddlem1  41267  ovnhoi  41300  hspdifhsp  41313  0setrec  43019
  Copyright terms: Public domain W3C validator