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

Theorem sseqin2 3779
Description: A relationship between subclass and intersection. Similar to Exercise 9 of [TakeutiZaring] p. 18. (Contributed by NM, 17-May-1994.)
Assertion
Ref Expression
sseqin2 (𝐴𝐵 ↔ (𝐵𝐴) = 𝐴)

Proof of Theorem sseqin2
StepHypRef Expression
1 df-ss 3554 . 2 (𝐴𝐵 ↔ (𝐴𝐵) = 𝐴)
2 incom 3767 . . 3 (𝐴𝐵) = (𝐵𝐴)
32eqeq1i 2615 . 2 ((𝐴𝐵) = 𝐴 ↔ (𝐵𝐴) = 𝐴)
41, 3bitri 263 1 (𝐴𝐵 ↔ (𝐵𝐴) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 195   = wceq 1475  cin 3539  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-nfc 2740  df-v 3175  df-in 3547  df-ss 3554
This theorem is referenced by:  dfss5OLD  3781  sseqin2OLD  3794  dfss4  3820  rintn0  4552  resabs1  5347  resima2  5352  xpssres  5354  rescnvcnv  5515  sspred  5605  onfr  5680  ordtri2or3  5741  fndmdif  6229  fimacnvinrn2  6257  fveqressseq  6263  sorpssin  6843  predon  6883  omsinds  6976  frnsuppeq  7194  wfrlem4  7305  fiint  8122  infxpenlem  8719  acndom2  8760  ackbij1lem2  8926  isf34lem5  9083  fpwwe2  9344  uzin  11596  iooval2  12079  fzval2  12200  leiso  13100  fz1isolem  13102  isercolllem3  14245  incexc  14408  bitsinv1  15002  bitsinvp1  15009  bitsshft  15035  dfphi2  15317  ressbas  15757  ressress  15765  ressabs  15766  psssdm  17039  sylow3lem2  17866  gsumxp  18198  dprdsn  18258  ablfac1eu  18295  pgpfac1lem5  18301  ablfaclem3  18309  ocv1  19842  resttopon  20775  restabs  20779  restopnb  20789  restperf  20798  ordtbas  20806  ordtrest2lem  20817  ordtrest2  20818  leordtvallem1  20824  leordtvallem2  20825  cnclsi  20886  ordtt1  20993  cmpsub  21013  connsub  21034  cnconn  21035  nconsubb  21036  consubclo  21037  1stcfb  21058  kgentopon  21151  ptbasfi  21194  ptclsg  21228  dfac14lem  21230  xkoccn  21232  txcnmpt  21237  txtube  21253  xkoptsub  21267  xkopt  21268  kqsat  21344  kqcldsat  21346  ordthmeolem  21414  fbasrn  21498  trfil1  21500  trfil2  21501  trufil  21524  qustgphaus  21736  trust  21843  metustfbas  22172  cfilucfil  22174  xrsmopn  22423  lebnumii  22573  iscmet3  22899  resscdrg  22962  cmmbl  23109  voliunlem3  23127  uniioombllem4  23160  mbflimsup  23239  0plef  23245  0pledm  23246  itg1ge0  23259  mbfi1fseqlem5  23292  itg2addlem  23331  dvcmulf  23514  lhop1  23581  lhop2  23582  efopn  24204  wilthlem2  24595  ex-in  26674  cmcmlem  27834  pjvec  27939  pjocvec  27940  ssmd2  28555  mdslmd4i  28576  chirredlem2  28634  chirredlem3  28635  dmdbr7ati  28667  difuncomp  28752  xppreima  28829  gtiso  28861  resf1o  28893  prsss  29290  ordtrestNEW  29295  ordtrest2NEWlem  29296  ordtrest2NEW  29297  lmxrge0  29326  carsggect  29707  probdsb  29811  totprobd  29815  cndprobtot  29825  orvcelval  29857  ballotlemfmpn  29883  signsplypnf  29953  signsply0  29954  dfon2lem4  30935  frrlem4  31027  neibastop3  31527  bj-restsnss  32217  topdifinfeq  32374  poimirlem3  32582  poimirlem9  32588  mblfinlem3  32618  mblfinlem4  32619  itg2addnclem2  32632  blssp  32722  sstotbnd2  32743  lcvexchlem1  33339  lcvexchlem4  33342  glbconN  33681  pmapglb2N  34075  pmapglb2xN  34076  2polssN  34219  polatN  34235  osumcllem1N  34260  osumcllem9N  34268  pexmidlem6N  34279  diarnN  35436  dihmeetlem11N  35624  dochexmidlem6  35772  lclkrlem2r  35831  mapdunirnN  35957  rfovcnvf1od  37318  fsovcnvlem  37327  ntrneifv3  37400  ntrneifv4  37403  clsneifv3  37428  clsneifv4  37429  neicvgfv  37439  k0004lem2  37466  wnefimgd  37480  inabs3  38249  stoweidlem50  38943  sge0iunmptlemre  39308  caratheodorylem1  39416  smfconst  39636
  Copyright terms: Public domain W3C validator