Theorem sseqin2 4164

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

Step	Hyp	Ref	Expression
1		dfss2 3908	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2		ineqcom 4151	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 ↔ (𝐵 ∩ 𝐴) = 𝐴)
3	1, 2	bitri 275	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∩ 𝐴) = 𝐴)

Syntax hints:   ↔ wb 206   = wceq 1542   ∩ cin 3889   ⊆ wss 3890

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-in 3897  df-ss 3907

This theorem is referenced by:  dfss4  4210  rintn0  5052  resabs1  5972  resima2  5982  xpssres  5984  mptimass  6039  rescnvcnv  6169  sspred  6275  trpred  6296  predres  6304  onfr  6363  ordtri2or3  6426  fndmdif  6995  fimacnvinrn2  7025  fveqressseq  7032  sorpssin  7685  cnvoprab  8013  frpoins3xpg  8090  frpoins3xp3g  8091  xpord3pred  8102  fsuppeq  8125  fsuppeqg  8126  frrlem4  8239  fiint  9237  infxpenlem  9935  acndom2  9976  ackbij1lem2  10142  isf34lem5  10300  fpwwe2  10566  uzin  12824  iooval2  13331  fzval2  13464  leiso  14421  fz1isolem  14423  isercolllem3  15629  incexc  15802  bitsinv1  16411  bitsinvp1  16418  bitsshft  16444  dfphi2  16744  ressbas  17206  ressress  17217  ressabs  17218  psssdm  18548  sylow3lem2  19603  gsumxp  19951  dprdsn  20013  ablfac1eu  20050  pgpfac1lem5  20056  ablfaclem3  20064  ocv1  21659  resttopon  23126  restabs  23130  restopnb  23140  restperf  23149  ordtbas  23157  ordtrest2lem  23168  ordtrest2  23169  leordtvallem1  23175  leordtvallem2  23176  cnclsi  23237  ordtt1  23344  cmpsub  23365  connsub  23386  cnconn  23387  nconnsubb  23388  connsubclo  23389  1stcfb  23410  kgentopon  23503  ptbasfi  23546  ptclsg  23580  dfac14lem  23582  xkoccn  23584  txcnmpt  23589  txtube  23605  xkoptsub  23619  xkopt  23620  kqsat  23696  kqcldsat  23698  ordthmeolem  23766  fbasrn  23849  trfil1  23851  trfil2  23852  trufil  23875  qustgphaus  24088  trust  24194  metustfbas  24522  cfilucfil  24524  xrsmopn  24778  lebnumii  24933  iscmet3  25260  resscdrg  25325  cmmbl  25501  voliunlem3  25519  uniioombllem4  25553  mbflimsup  25633  0plef  25639  0pledm  25640  itg1ge0  25653  mbfi1fseqlem5  25686  itg2addlem  25725  dvcmulf  25912  lhop1  25981  lhop2  25982  efopn  26622  wilthlem2  27032  ex-in  30495  cmcmlem  31662  pjvec  31767  pjocvec  31768  ssmd2  32383  mdslmd4i  32404  chirredlem2  32462  chirredlem3  32463  dmdbr7ati  32495  difuncomp  32623  xppreima  32718  partfun2  32749  suppovss  32754  fressupp  32761  gtiso  32774  preiman0  32783  fsuppcurry1  32797  fsuppcurry2  32798  resf1o  32803  elrgspnsubrunlem2  33309  elrspunidl  33488  ply1degltdimlem  33766  fldgenfldext  33812  rspectopn  34011  prsss  34060  ordtrestNEW  34065  ordtrest2NEWlem  34066  ordtrest2NEW  34067  lmxrge0  34096  carsggect  34462  probdsb  34566  totprobd  34570  cndprobtot  34580  orvcelval  34613  ballotlemfmpn  34639  signsplypnf  34694  signsply0  34695  dfon2lem4  35966  neibastop3  36544  weiunfrlem  36646  bj-restsnss  37395  bj-ismoored2  37420  bj-inexeqex  37468  bj-idreseq  37476  topdifinfeq  37666  poimirlem3  37944  poimirlem9  37950  mblfinlem3  37980  mblfinlem4  37981  itg2addnclem2  37993  blssp  38077  sstotbnd2  38095  lcvexchlem1  39480  lcvexchlem4  39483  glbconN  39823  pmapglb2N  40217  pmapglb2xN  40218  2polssN  40361  polatN  40377  osumcllem1N  40402  osumcllem9N  40410  pexmidlem6N  40421  diarnN  41575  dihmeetlem11N  41763  dochexmidlem6  41911  lclkrlem2r  41970  mapdunirnN  42096  fsuppssindlem2  43025  prjcrv0  43066  ofoafg  43782  harval3  43965  rfovcnvf1od  44431  fsovcnvlem  44440  ntrneifv3  44509  ntrneifv4  44512  clsneifv3  44537  clsneifv4  44538  neicvgfv  44548  k0004lem2  44575  wnefimgd  44588  inabs3  45487  stoweidlem50  46478  sge0iunmptlemre  46843  caratheodorylem1  46954  smfconst  47177  fresfo  47490  funfocofob  47520  grimuhgr  48357  restclsseplem  49384  incat  50070