Theorem sseqin2 4176

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∩ cin 3904   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-in 3912  df-ss 3922

This theorem is referenced by:  dfss4  4222  rintn0  5061  resabs1  5961  resima2  5971  xpssres  5973  mptimass  6028  rescnvcnv  6157  sspred  6262  trpred  6283  predres  6291  onfr  6350  ordtri2or3  6413  fndmdif  6980  fimacnvinrn2  7010  fveqressseq  7017  sorpssin  7671  cnvoprab  8002  frpoins3xpg  8080  frpoins3xp3g  8081  xpord3pred  8092  fsuppeq  8115  fsuppeqg  8116  frrlem4  8229  fiint  9235  fiintOLD  9236  infxpenlem  9926  acndom2  9967  ackbij1lem2  10133  isf34lem5  10291  fpwwe2  10556  uzin  12793  iooval2  13299  fzval2  13431  leiso  14384  fz1isolem  14386  isercolllem3  15592  incexc  15762  bitsinv1  16371  bitsinvp1  16378  bitsshft  16404  dfphi2  16703  ressbas  17165  ressress  17176  ressabs  17177  psssdm  18506  sylow3lem2  19525  gsumxp  19873  dprdsn  19935  ablfac1eu  19972  pgpfac1lem5  19978  ablfaclem3  19986  ocv1  21604  resttopon  23064  restabs  23068  restopnb  23078  restperf  23087  ordtbas  23095  ordtrest2lem  23106  ordtrest2  23107  leordtvallem1  23113  leordtvallem2  23114  cnclsi  23175  ordtt1  23282  cmpsub  23303  connsub  23324  cnconn  23325  nconnsubb  23326  connsubclo  23327  1stcfb  23348  kgentopon  23441  ptbasfi  23484  ptclsg  23518  dfac14lem  23520  xkoccn  23522  txcnmpt  23527  txtube  23543  xkoptsub  23557  xkopt  23558  kqsat  23634  kqcldsat  23636  ordthmeolem  23704  fbasrn  23787  trfil1  23789  trfil2  23790  trufil  23813  qustgphaus  24026  trust  24133  metustfbas  24461  cfilucfil  24463  xrsmopn  24717  lebnumii  24881  iscmet3  25209  resscdrg  25274  cmmbl  25451  voliunlem3  25469  uniioombllem4  25503  mbflimsup  25583  0plef  25589  0pledm  25590  itg1ge0  25603  mbfi1fseqlem5  25636  itg2addlem  25675  dvcmulf  25864  lhop1  25935  lhop2  25936  efopn  26583  wilthlem2  26995  ex-in  30387  cmcmlem  31553  pjvec  31658  pjocvec  31659  ssmd2  32274  mdslmd4i  32295  chirredlem2  32353  chirredlem3  32354  dmdbr7ati  32386  difuncomp  32515  xppreima  32602  suppovss  32637  fressupp  32644  gtiso  32657  preiman0  32666  fsuppcurry1  32681  fsuppcurry2  32682  resf1o  32686  elrgspnsubrunlem2  33198  elrspunidl  33375  ply1degltdimlem  33594  fldgenfldext  33639  rspectopn  33833  prsss  33882  ordtrestNEW  33887  ordtrest2NEWlem  33888  ordtrest2NEW  33889  lmxrge0  33918  carsggect  34285  probdsb  34389  totprobd  34393  cndprobtot  34403  orvcelval  34436  ballotlemfmpn  34462  signsplypnf  34517  signsply0  34518  dfon2lem4  35759  neibastop3  36335  weiunfrlem  36437  bj-restsnss  37056  bj-ismoored2  37081  bj-inexeqex  37127  bj-idreseq  37135  topdifinfeq  37323  poimirlem3  37602  poimirlem9  37608  mblfinlem3  37638  mblfinlem4  37639  itg2addnclem2  37651  blssp  37735  sstotbnd2  37753  lcvexchlem1  39012  lcvexchlem4  39015  glbconN  39355  glbconNOLD  39356  pmapglb2N  39750  pmapglb2xN  39751  2polssN  39894  polatN  39910  osumcllem1N  39935  osumcllem9N  39943  pexmidlem6N  39954  diarnN  41108  dihmeetlem11N  41296  dochexmidlem6  41444  lclkrlem2r  41503  mapdunirnN  41629  fsuppssindlem2  42565  prjcrv0  42606  ofoafg  43327  harval3  43511  rfovcnvf1od  43977  fsovcnvlem  43986  ntrneifv3  44055  ntrneifv4  44058  clsneifv3  44083  clsneifv4  44084  neicvgfv  44094  k0004lem2  44121  wnefimgd  44134  inabs3  45034  stoweidlem50  46032  sge0iunmptlemre  46397  caratheodorylem1  46508  smfconst  46731  fresfo  47033  funfocofob  47063  grimuhgr  47871  restclsseplem  48887  incat  49574