Theorem sseqin2 4194

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 3954	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2		incom 4180	. . 3 ⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴)
3	2	eqeq1i 2828	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 ↔ (𝐵 ∩ 𝐴) = 𝐴)
4	1, 3	bitri 277	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∩ 𝐴) = 𝐴)

Syntax hints:   ↔ wb 208   = wceq 1537   ∩ cin 3937   ⊆ wss 3938

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1540  df-ex 1781  df-sb 2070  df-clab 2802  df-cleq 2816  df-rab 3149  df-in 3945  df-ss 3954

This theorem is referenced by:  dfss4  4237  rintn0  5032  resabs1  5885  resima2  5890  xpssres  5891  rescnvcnv  6063  sspred  6158  onfr  6232  ordtri2or3  6290  fndmdif  6814  fimacnvinrn2  6843  fveqressseq  6849  sorpssin  7459  predon  7508  omsinds  7602  cnvoprab  7760  frnsuppeq  7844  wfrlem4  7960  fiint  8797  infxpenlem  9441  acndom2  9482  ackbij1lem2  9645  isf34lem5  9802  fpwwe2  10067  uzin  12281  iooval2  12774  fzval2  12898  leiso  13820  fz1isolem  13822  isercolllem3  15025  incexc  15194  bitsinv1  15793  bitsinvp1  15800  bitsshft  15826  dfphi2  16113  ressbas  16556  ressress  16564  ressabs  16565  psssdm  17828  sylow3lem2  18755  gsumxp  19098  dprdsn  19160  ablfac1eu  19197  pgpfac1lem5  19203  ablfaclem3  19211  ocv1  20825  resttopon  21771  restabs  21775  restopnb  21785  restperf  21794  ordtbas  21802  ordtrest2lem  21813  ordtrest2  21814  leordtvallem1  21820  leordtvallem2  21821  cnclsi  21882  ordtt1  21989  cmpsub  22010  connsub  22031  cnconn  22032  nconnsubb  22033  connsubclo  22034  1stcfb  22055  kgentopon  22148  ptbasfi  22191  ptclsg  22225  dfac14lem  22227  xkoccn  22229  txcnmpt  22234  txtube  22250  xkoptsub  22264  xkopt  22265  kqsat  22341  kqcldsat  22343  ordthmeolem  22411  fbasrn  22494  trfil1  22496  trfil2  22497  trufil  22520  qustgphaus  22733  trust  22840  metustfbas  23169  cfilucfil  23171  xrsmopn  23422  lebnumii  23572  iscmet3  23898  resscdrg  23963  cmmbl  24137  voliunlem3  24155  uniioombllem4  24189  mbflimsup  24269  0plef  24275  0pledm  24276  itg1ge0  24289  mbfi1fseqlem5  24322  itg2addlem  24361  dvcmulf  24544  lhop1  24613  lhop2  24614  efopn  25243  wilthlem2  25648  ex-in  28206  cmcmlem  29370  pjvec  29475  pjocvec  29476  ssmd2  30091  mdslmd4i  30112  chirredlem2  30170  chirredlem3  30171  dmdbr7ati  30203  difuncomp  30307  xppreima  30396  suppovss  30428  gtiso  30438  fsuppcurry1  30463  fsuppcurry2  30464  resf1o  30468  prsss  31161  ordtrestNEW  31166  ordtrest2NEWlem  31167  ordtrest2NEW  31168  lmxrge0  31197  carsggect  31578  probdsb  31682  totprobd  31686  cndprobtot  31696  orvcelval  31728  ballotlemfmpn  31754  signsplypnf  31822  signsply0  31823  dfon2lem4  33033  frrlem4  33128  neibastop3  33712  bj-restsnss  34376  bj-ismoored2  34402  bj-inexeqex  34448  bj-idreseq  34456  topdifinfeq  34633  poimirlem3  34897  poimirlem9  34903  mblfinlem3  34933  mblfinlem4  34934  itg2addnclem2  34946  blssp  35033  sstotbnd2  35054  lcvexchlem1  36172  lcvexchlem4  36175  glbconN  36515  pmapglb2N  36909  pmapglb2xN  36910  2polssN  37053  polatN  37069  osumcllem1N  37094  osumcllem9N  37102  pexmidlem6N  37113  diarnN  38267  dihmeetlem11N  38455  dochexmidlem6  38603  lclkrlem2r  38662  mapdunirnN  38788  harval3  39911  rfovcnvf1od  40357  fsovcnvlem  40366  ntrneifv3  40439  ntrneifv4  40442  clsneifv3  40467  clsneifv4  40468  neicvgfv  40478  k0004lem2  40505  wnefimgd  40519  inabs3  41325  mptima2  41524  stoweidlem50  42342  sge0iunmptlemre  42704  caratheodorylem1  42815  smfconst  43033