Theorem sseqin2 4146

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		df-ss 3900	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2		incom 4131	. . 3 ⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴)
3	2	eqeq1i 2743	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 ↔ (𝐵 ∩ 𝐴) = 𝐴)
4	1, 3	bitri 274	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∩ 𝐴) = 𝐴)

Syntax hints:   ↔ wb 205   = wceq 1539   ∩ cin 3882   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-rab 3072  df-in 3890  df-ss 3900

This theorem is referenced by:  dfss4  4189  rintn0  5034  resabs1  5910  resima2  5915  xpssres  5917  rescnvcnv  6096  sspred  6200  trpred  6223  onfr  6290  ordtri2or3  6348  fndmdif  6901  fimacnvinrn2  6932  fveqressseq  6939  sorpssin  7562  predonOLD  7613  omsindsOLD  7709  cnvoprab  7873  frnsuppeq  7962  frnsuppeqg  7963  frrlem4  8076  wfrlem4OLD  8114  fiint  9021  infxpenlem  9700  acndom2  9741  ackbij1lem2  9908  isf34lem5  10065  fpwwe2  10330  uzin  12547  iooval2  13041  fzval2  13171  leiso  14101  fz1isolem  14103  isercolllem3  15306  incexc  15477  bitsinv1  16077  bitsinvp1  16084  bitsshft  16110  dfphi2  16403  ressbas  16873  ressbasOLD  16874  ressress  16884  ressabs  16885  psssdm  18215  sylow3lem2  19148  gsumxp  19492  dprdsn  19554  ablfac1eu  19591  pgpfac1lem5  19597  ablfaclem3  19605  ocv1  20796  resttopon  22220  restabs  22224  restopnb  22234  restperf  22243  ordtbas  22251  ordtrest2lem  22262  ordtrest2  22263  leordtvallem1  22269  leordtvallem2  22270  cnclsi  22331  ordtt1  22438  cmpsub  22459  connsub  22480  cnconn  22481  nconnsubb  22482  connsubclo  22483  1stcfb  22504  kgentopon  22597  ptbasfi  22640  ptclsg  22674  dfac14lem  22676  xkoccn  22678  txcnmpt  22683  txtube  22699  xkoptsub  22713  xkopt  22714  kqsat  22790  kqcldsat  22792  ordthmeolem  22860  fbasrn  22943  trfil1  22945  trfil2  22946  trufil  22969  qustgphaus  23182  trust  23289  metustfbas  23619  cfilucfil  23621  xrsmopn  23881  lebnumii  24035  iscmet3  24362  resscdrg  24427  cmmbl  24603  voliunlem3  24621  uniioombllem4  24655  mbflimsup  24735  0plef  24741  0pledm  24742  itg1ge0  24755  mbfi1fseqlem5  24789  itg2addlem  24828  dvcmulf  25014  lhop1  25083  lhop2  25084  efopn  25718  wilthlem2  26123  ex-in  28690  cmcmlem  29854  pjvec  29959  pjocvec  29960  ssmd2  30575  mdslmd4i  30596  chirredlem2  30654  chirredlem3  30655  dmdbr7ati  30687  difuncomp  30794  xppreima  30884  suppovss  30919  fressupp  30924  gtiso  30935  preiman0  30944  fsuppcurry1  30962  fsuppcurry2  30963  resf1o  30967  elrspunidl  31508  rspectopn  31719  prsss  31768  ordtrestNEW  31773  ordtrest2NEWlem  31774  ordtrest2NEW  31775  lmxrge0  31804  carsggect  32185  probdsb  32289  totprobd  32293  cndprobtot  32303  orvcelval  32335  ballotlemfmpn  32361  signsplypnf  32429  signsply0  32430  dfon2lem4  33668  frpoins3xpg  33714  frpoins3xp3g  33715  xpord3pred  33725  neibastop3  34478  bj-restsnss  35181  bj-ismoored2  35206  bj-inexeqex  35252  bj-idreseq  35260  topdifinfeq  35448  poimirlem3  35707  poimirlem9  35713  mblfinlem3  35743  mblfinlem4  35744  itg2addnclem2  35756  blssp  35841  sstotbnd2  35859  lcvexchlem1  36975  lcvexchlem4  36978  glbconN  37318  pmapglb2N  37712  pmapglb2xN  37713  2polssN  37856  polatN  37872  osumcllem1N  37897  osumcllem9N  37905  pexmidlem6N  37916  diarnN  39070  dihmeetlem11N  39258  dochexmidlem6  39406  lclkrlem2r  39465  mapdunirnN  39591  fsuppssindlem2  40204  harval3  41041  rfovcnvf1od  41501  fsovcnvlem  41510  ntrneifv3  41581  ntrneifv4  41584  clsneifv3  41609  clsneifv4  41610  neicvgfv  41620  k0004lem2  41647  wnefimgd  41661  inabs3  42493  mptima2  42680  stoweidlem50  43481  sge0iunmptlemre  43843  caratheodorylem1  43954  smfconst  44172  fresfo  44429  funfocofob  44457  restclsseplem  46096