Theorem sseqin2 4177

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 3921	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2		incom 4163	. . 3 ⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴)
3	2	eqeq1i 2742	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 ↔ (𝐵 ∩ 𝐴) = 𝐴)
4	1, 3	bitri 275	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∩ 𝐴) = 𝐴)

Syntax hints:   ↔ wb 206   = wceq 1542   ∩ cin 3902   ⊆ wss 3903

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 3402  df-in 3910  df-ss 3920

This theorem is referenced by:  dfss4  4223  rintn0  5066  resabs1  5973  resima2  5983  xpssres  5985  mptimass  6040  rescnvcnv  6170  sspred  6276  trpred  6297  predres  6305  onfr  6364  ordtri2or3  6427  fndmdif  6996  fimacnvinrn2  7026  fveqressseq  7033  sorpssin  7686  cnvoprab  8014  frpoins3xpg  8092  frpoins3xp3g  8093  xpord3pred  8104  fsuppeq  8127  fsuppeqg  8128  frrlem4  8241  fiint  9239  infxpenlem  9935  acndom2  9976  ackbij1lem2  10142  isf34lem5  10300  fpwwe2  10566  uzin  12799  iooval2  13306  fzval2  13438  leiso  14394  fz1isolem  14396  isercolllem3  15602  incexc  15772  bitsinv1  16381  bitsinvp1  16388  bitsshft  16414  dfphi2  16713  ressbas  17175  ressress  17186  ressabs  17187  psssdm  18517  sylow3lem2  19569  gsumxp  19917  dprdsn  19979  ablfac1eu  20016  pgpfac1lem5  20022  ablfaclem3  20030  ocv1  21646  resttopon  23117  restabs  23121  restopnb  23131  restperf  23140  ordtbas  23148  ordtrest2lem  23159  ordtrest2  23160  leordtvallem1  23166  leordtvallem2  23167  cnclsi  23228  ordtt1  23335  cmpsub  23356  connsub  23377  cnconn  23378  nconnsubb  23379  connsubclo  23380  1stcfb  23401  kgentopon  23494  ptbasfi  23537  ptclsg  23571  dfac14lem  23573  xkoccn  23575  txcnmpt  23580  txtube  23596  xkoptsub  23610  xkopt  23611  kqsat  23687  kqcldsat  23689  ordthmeolem  23757  fbasrn  23840  trfil1  23842  trfil2  23843  trufil  23866  qustgphaus  24079  trust  24185  metustfbas  24513  cfilucfil  24515  xrsmopn  24769  lebnumii  24933  iscmet3  25261  resscdrg  25326  cmmbl  25503  voliunlem3  25521  uniioombllem4  25555  mbflimsup  25635  0plef  25641  0pledm  25642  itg1ge0  25655  mbfi1fseqlem5  25688  itg2addlem  25727  dvcmulf  25916  lhop1  25987  lhop2  25988  efopn  26635  wilthlem2  27047  ex-in  30512  cmcmlem  31678  pjvec  31783  pjocvec  31784  ssmd2  32399  mdslmd4i  32420  chirredlem2  32478  chirredlem3  32479  dmdbr7ati  32511  difuncomp  32639  xppreima  32734  partfun2  32765  suppovss  32770  fressupp  32777  gtiso  32790  preiman0  32799  fsuppcurry1  32813  fsuppcurry2  32814  resf1o  32819  elrgspnsubrunlem2  33341  elrspunidl  33520  ply1degltdimlem  33799  fldgenfldext  33845  rspectopn  34044  prsss  34093  ordtrestNEW  34098  ordtrest2NEWlem  34099  ordtrest2NEW  34100  lmxrge0  34129  carsggect  34495  probdsb  34599  totprobd  34603  cndprobtot  34613  orvcelval  34646  ballotlemfmpn  34672  signsplypnf  34727  signsply0  34728  dfon2lem4  35997  neibastop3  36575  weiunfrlem  36677  bj-restsnss  37327  bj-ismoored2  37352  bj-inexeqex  37398  bj-idreseq  37406  topdifinfeq  37594  poimirlem3  37863  poimirlem9  37869  mblfinlem3  37899  mblfinlem4  37900  itg2addnclem2  37912  blssp  37996  sstotbnd2  38014  lcvexchlem1  39399  lcvexchlem4  39402  glbconN  39742  pmapglb2N  40136  pmapglb2xN  40137  2polssN  40280  polatN  40296  osumcllem1N  40321  osumcllem9N  40329  pexmidlem6N  40340  diarnN  41494  dihmeetlem11N  41682  dochexmidlem6  41830  lclkrlem2r  41889  mapdunirnN  42015  fsuppssindlem2  42939  prjcrv0  42980  ofoafg  43700  harval3  43883  rfovcnvf1od  44349  fsovcnvlem  44358  ntrneifv3  44427  ntrneifv4  44430  clsneifv3  44455  clsneifv4  44456  neicvgfv  44466  k0004lem2  44493  wnefimgd  44506  inabs3  45405  stoweidlem50  46397  sge0iunmptlemre  46762  caratheodorylem1  46873  smfconst  47096  fresfo  47397  funfocofob  47427  grimuhgr  48236  restclsseplem  49263  incat  49949