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

Theorem sseqin2 4191
 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 3951 . 2 (𝐴𝐵 ↔ (𝐴𝐵) = 𝐴)
2 incom 4177 . . 3 (𝐴𝐵) = (𝐵𝐴)
32eqeq1i 2826 . 2 ((𝐴𝐵) = 𝐴 ↔ (𝐵𝐴) = 𝐴)
41, 3bitri 277 1 (𝐴𝐵 ↔ (𝐵𝐴) = 𝐴)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 208   = wceq 1533   ∩ cin 3934   ⊆ 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-9 2120  ax-ext 2793 This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1536  df-ex 1777  df-sb 2066  df-clab 2800  df-cleq 2814  df-rab 3147  df-in 3942  df-ss 3951 This theorem is referenced by:  dfss4  4234  rintn0  5029  resabs1  5882  resima2  5887  xpssres  5888  rescnvcnv  6060  sspred  6155  onfr  6229  ordtri2or3  6287  fndmdif  6811  fimacnvinrn2  6840  fveqressseq  6846  sorpssin  7456  predon  7505  omsinds  7599  cnvoprab  7757  frnsuppeq  7841  wfrlem4  7957  fiint  8794  infxpenlem  9438  acndom2  9479  ackbij1lem2  9642  isf34lem5  9799  fpwwe2  10064  uzin  12277  iooval2  12770  fzval2  12894  leiso  13816  fz1isolem  13818  isercolllem3  15022  incexc  15191  bitsinv1  15790  bitsinvp1  15797  bitsshft  15823  dfphi2  16110  ressbas  16553  ressress  16561  ressabs  16562  psssdm  17825  sylow3lem2  18752  gsumxp  19095  dprdsn  19157  ablfac1eu  19194  pgpfac1lem5  19200  ablfaclem3  19208  ocv1  20822  resttopon  21768  restabs  21772  restopnb  21782  restperf  21791  ordtbas  21799  ordtrest2lem  21810  ordtrest2  21811  leordtvallem1  21817  leordtvallem2  21818  cnclsi  21879  ordtt1  21986  cmpsub  22007  connsub  22028  cnconn  22029  nconnsubb  22030  connsubclo  22031  1stcfb  22052  kgentopon  22145  ptbasfi  22188  ptclsg  22222  dfac14lem  22224  xkoccn  22226  txcnmpt  22231  txtube  22247  xkoptsub  22261  xkopt  22262  kqsat  22338  kqcldsat  22340  ordthmeolem  22408  fbasrn  22491  trfil1  22493  trfil2  22494  trufil  22517  qustgphaus  22730  trust  22837  metustfbas  23166  cfilucfil  23168  xrsmopn  23419  lebnumii  23569  iscmet3  23895  resscdrg  23960  cmmbl  24134  voliunlem3  24152  uniioombllem4  24186  mbflimsup  24266  0plef  24272  0pledm  24273  itg1ge0  24286  mbfi1fseqlem5  24319  itg2addlem  24358  dvcmulf  24541  lhop1  24610  lhop2  24611  efopn  25240  wilthlem2  25645  ex-in  28203  cmcmlem  29367  pjvec  29472  pjocvec  29473  ssmd2  30088  mdslmd4i  30109  chirredlem2  30167  chirredlem3  30168  dmdbr7ati  30200  difuncomp  30304  xppreima  30393  suppovss  30425  gtiso  30435  fsuppcurry1  30460  fsuppcurry2  30461  resf1o  30465  prsss  31159  ordtrestNEW  31164  ordtrest2NEWlem  31165  ordtrest2NEW  31166  lmxrge0  31195  carsggect  31576  probdsb  31680  totprobd  31684  cndprobtot  31694  orvcelval  31726  ballotlemfmpn  31752  signsplypnf  31820  signsply0  31821  dfon2lem4  33031  frrlem4  33126  neibastop3  33710  bj-restsnss  34373  bj-ismoored2  34399  bj-inexeqex  34445  bj-idreseq  34453  topdifinfeq  34630  poimirlem3  34894  poimirlem9  34900  mblfinlem3  34930  mblfinlem4  34931  itg2addnclem2  34943  blssp  35030  sstotbnd2  35051  lcvexchlem1  36169  lcvexchlem4  36172  glbconN  36512  pmapglb2N  36906  pmapglb2xN  36907  2polssN  37050  polatN  37066  osumcllem1N  37091  osumcllem9N  37099  pexmidlem6N  37110  diarnN  38264  dihmeetlem11N  38452  dochexmidlem6  38600  lclkrlem2r  38659  mapdunirnN  38785  harval3  39902  rfovcnvf1od  40348  fsovcnvlem  40357  ntrneifv3  40430  ntrneifv4  40433  clsneifv3  40458  clsneifv4  40459  neicvgfv  40469  k0004lem2  40496  wnefimgd  40510  inabs3  41316  mptima2  41515  stoweidlem50  42334  sge0iunmptlemre  42696  caratheodorylem1  42807  smfconst  43025
 Copyright terms: Public domain W3C validator