Theorem sseqin2 4214

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

Syntax hints:   ↔ wb 205   = wceq 1542   ∩ cin 3946   ⊆ wss 3947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-rab 3434  df-in 3954  df-ss 3964

This theorem is referenced by:  dfss4  4257  rintn0  5111  resabs1  6009  resima2  6014  xpssres  6016  rescnvcnv  6200  sspred  6306  trpred  6329  predres  6337  onfr  6400  ordtri2or3  6461  fndmdif  7039  fimacnvinrn2  7070  fveqressseq  7077  sorpssin  7716  predonOLD  7769  omsindsOLD  7872  cnvoprab  8041  frpoins3xpg  8121  frpoins3xp3g  8122  xpord3pred  8133  fsuppeq  8155  fsuppeqg  8156  frrlem4  8269  wfrlem4OLD  8307  fiint  9320  infxpenlem  10004  acndom2  10045  ackbij1lem2  10212  isf34lem5  10369  fpwwe2  10634  uzin  12858  iooval2  13353  fzval2  13483  leiso  14416  fz1isolem  14418  isercolllem3  15609  incexc  15779  bitsinv1  16379  bitsinvp1  16386  bitsshft  16412  dfphi2  16703  ressbas  17175  ressbasOLD  17176  ressress  17189  ressabs  17190  psssdm  18531  sylow3lem2  19489  gsumxp  19836  dprdsn  19898  ablfac1eu  19935  pgpfac1lem5  19941  ablfaclem3  19949  ocv1  21216  resttopon  22647  restabs  22651  restopnb  22661  restperf  22670  ordtbas  22678  ordtrest2lem  22689  ordtrest2  22690  leordtvallem1  22696  leordtvallem2  22697  cnclsi  22758  ordtt1  22865  cmpsub  22886  connsub  22907  cnconn  22908  nconnsubb  22909  connsubclo  22910  1stcfb  22931  kgentopon  23024  ptbasfi  23067  ptclsg  23101  dfac14lem  23103  xkoccn  23105  txcnmpt  23110  txtube  23126  xkoptsub  23140  xkopt  23141  kqsat  23217  kqcldsat  23219  ordthmeolem  23287  fbasrn  23370  trfil1  23372  trfil2  23373  trufil  23396  qustgphaus  23609  trust  23716  metustfbas  24048  cfilucfil  24050  xrsmopn  24310  lebnumii  24464  iscmet3  24792  resscdrg  24857  cmmbl  25033  voliunlem3  25051  uniioombllem4  25085  mbflimsup  25165  0plef  25171  0pledm  25172  itg1ge0  25185  mbfi1fseqlem5  25219  itg2addlem  25258  dvcmulf  25444  lhop1  25513  lhop2  25514  efopn  26148  wilthlem2  26553  ex-in  29658  cmcmlem  30822  pjvec  30927  pjocvec  30928  ssmd2  31543  mdslmd4i  31564  chirredlem2  31622  chirredlem3  31623  dmdbr7ati  31655  difuncomp  31763  xppreima  31849  suppovss  31884  fressupp  31888  gtiso  31900  preiman0  31909  fsuppcurry1  31928  fsuppcurry2  31929  resf1o  31933  elrspunidl  32504  ply1degltdimlem  32652  rspectopn  32785  prsss  32834  ordtrestNEW  32839  ordtrest2NEWlem  32840  ordtrest2NEW  32841  lmxrge0  32870  carsggect  33255  probdsb  33359  totprobd  33363  cndprobtot  33373  orvcelval  33405  ballotlemfmpn  33431  signsplypnf  33499  signsply0  33500  dfon2lem4  34696  neibastop3  35185  bj-restsnss  35902  bj-ismoored2  35927  bj-inexeqex  35973  bj-idreseq  35981  topdifinfeq  36169  poimirlem3  36429  poimirlem9  36435  mblfinlem3  36465  mblfinlem4  36466  itg2addnclem2  36478  blssp  36562  sstotbnd2  36580  lcvexchlem1  37842  lcvexchlem4  37845  glbconN  38185  glbconNOLD  38186  pmapglb2N  38580  pmapglb2xN  38581  2polssN  38724  polatN  38740  osumcllem1N  38765  osumcllem9N  38773  pexmidlem6N  38784  diarnN  39938  dihmeetlem11N  40126  dochexmidlem6  40274  lclkrlem2r  40333  mapdunirnN  40459  fsuppssindlem2  41114  prjcrv0  41319  ofoafg  42037  harval3  42222  rfovcnvf1od  42688  fsovcnvlem  42697  ntrneifv3  42766  ntrneifv4  42769  clsneifv3  42794  clsneifv4  42795  neicvgfv  42805  k0004lem2  42832  wnefimgd  42846  inabs3  43676  mptima2  43884  stoweidlem50  44701  sge0iunmptlemre  45066  caratheodorylem1  45177  smfconst  45400  fresfo  45693  funfocofob  45721  restclsseplem  47449