Theorem sseqin2 4170

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 3917	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2		ineqcom 4157	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 ↔ (𝐵 ∩ 𝐴) = 𝐴)
3	1, 2	bitri 277	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∩ 𝐴) = 𝐴)

Syntax hints:   ↔ wb 208   = wceq 1554   ∩ cin 3898   ⊆ wss 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728

This theorem depends on definitions:  df-bi 209  df-an 399  df-3an 1097  df-tru 1557  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-rab 3409  df-in 3906  df-ss 3916

This theorem is referenced by:  dfss4  4216  rintn0  5060  resabs1  5985  resima2  5995  xpssres  5997  mptimass  6052  rescnvcnv  6180  sspred  6286  trpred  6307  predres  6315  onfr  6374  ordtri2or3  6437  fndmdif  7012  fimacnvinrn2  7042  fveqressseq  7049  sorpssin  7703  cnvoprab  8030  frpoins3xpg  8108  frpoins3xp3g  8109  xpord3pred  8120  fsuppeq  8143  fsuppeqg  8144  frrlem4  8258  fiint  9260  infxpenlem  9959  acndom2  10000  ackbij1lem2  10166  isf34lem5  10325  fpwwe2  10591  uzin  12865  iooval2  13372  fzval2  13505  leiso  14462  fz1isolem  14464  isercolllem3  15670  incexc  15843  bitsinv1  16452  bitsinvp1  16459  bitsshft  16485  dfphi2  16785  ressbas  17248  ressress  17259  ressabs  17260  psssdm  18590  sylow3lem2  19644  gsumxp  19992  dprdsn  20054  ablfac1eu  20091  pgpfac1lem5  20097  ablfaclem3  20105  ocv1  21704  resttopon  23194  restabs  23198  restopnb  23208  restperf  23217  ordtbas  23225  ordtrest2lem  23236  ordtrest2  23237  leordtvallem1  23243  leordtvallem2  23244  cnclsi  23305  ordtt1  23412  cmpsub  23433  connsub  23454  cnconn  23455  nconnsubb  23456  connsubclo  23457  1stcfb  23478  kgentopon  23571  ptbasfi  23614  ptclsg  23648  dfac14lem  23650  xkoccn  23652  txcnmpt  23657  txtube  23673  xkoptsub  23687  xkopt  23688  kqsat  23764  kqcldsat  23766  ordthmeolem  23834  fbasrn  23917  trfil1  23919  trfil2  23920  trufil  23943  qustgphaus  24156  trust  24262  metustfbas  24590  cfilucfil  24592  xrsmopn  24846  lebnumii  25001  iscmet3  25328  resscdrg  25393  cmmbl  25569  voliunlem3  25587  uniioombllem4  25621  mbflimsup  25701  0plef  25707  0pledm  25708  itg1ge0  25721  mbfi1fseqlem5  25754  itg2addlem  25793  dvcmulf  25980  lhop1  26049  lhop2  26050  efopn  26693  wilthlem2  27103  ex-in  30566  cmcmlem  31733  pjvec  31838  pjocvec  31839  ssmd2  32454  mdslmd4i  32475  chirredlem2  32533  chirredlem3  32534  dmdbr7ati  32566  difuncomp  32695  xppreima  32790  partfun2  32821  suppovss  32826  fressupp  32833  gtiso  32846  preiman0  32855  fsuppcurry1  32869  fsuppcurry2  32870  resf1o  32875  elrgspnsubrunlem2  33383  elrspunidl  33568  ply1degltdimlem  33873  fldgenfldext  33919  rspectopn  34118  prsss  34167  ordtrestNEW  34172  ordtrest2NEWlem  34173  ordtrest2NEW  34174  lmxrge0  34203  carsggect  34569  probdsb  34673  totprobd  34677  cndprobtot  34687  orvcelval  34720  ballotlemfmpn  34746  signsplypnf  34801  signsply0  34802  dfon2lem4  36082  neibastop3  36670  weiunfrlem  36772  bj-restsnss  37521  bj-ismoored2  37546  bj-inexeqex  37594  bj-idreseq  37602  topdifinfeq  37792  poimirlem3  38070  poimirlem9  38076  mblfinlem3  38106  mblfinlem4  38107  itg2addnclem2  38119  blssp  38203  sstotbnd2  38221  lcvexchlem1  39606  lcvexchlem4  39609  glbconN  39949  pmapglb2N  40343  pmapglb2xN  40344  2polssN  40487  polatN  40503  osumcllem1N  40528  osumcllem9N  40536  pexmidlem6N  40547  diarnN  41701  dihmeetlem11N  41889  dochexmidlem6  42037  lclkrlem2r  42096  mapdunirnN  42222  fsuppssindlem2  43122  prjcrv0  43163  ofoafg  43879  harval3  44062  rfovcnvf1od  44528  fsovcnvlem  44537  ntrneifv3  44606  ntrneifv4  44609  clsneifv3  44634  clsneifv4  44635  neicvgfv  44645  k0004lem2  44672  wnefimgd  44685  inabs3  45584  stoweidlem50  46572  sge0iunmptlemre  46937  caratheodorylem1  47048  smfconst  47271  fresfo  47590  funfocofob  47620  grimuhgr  48457  restclsseplem  49484  incat  50170