Theorem sseqin2 4171

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

Syntax hints:   ↔ wb 206   = wceq 1541   ∩ cin 3899   ⊆ wss 3900

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 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3394  df-in 3907  df-ss 3917

This theorem is referenced by:  dfss4  4217  rintn0  5055  resabs1  5952  resima2  5962  xpssres  5964  mptimass  6019  rescnvcnv  6148  sspred  6253  trpred  6274  predres  6282  onfr  6341  ordtri2or3  6404  fndmdif  6970  fimacnvinrn2  7000  fveqressseq  7007  sorpssin  7659  cnvoprab  7987  frpoins3xpg  8065  frpoins3xp3g  8066  xpord3pred  8077  fsuppeq  8100  fsuppeqg  8101  frrlem4  8214  fiint  9206  infxpenlem  9896  acndom2  9937  ackbij1lem2  10103  isf34lem5  10261  fpwwe2  10526  uzin  12764  iooval2  13270  fzval2  13402  leiso  14358  fz1isolem  14360  isercolllem3  15566  incexc  15736  bitsinv1  16345  bitsinvp1  16352  bitsshft  16378  dfphi2  16677  ressbas  17139  ressress  17150  ressabs  17151  psssdm  18480  sylow3lem2  19533  gsumxp  19881  dprdsn  19943  ablfac1eu  19980  pgpfac1lem5  19986  ablfaclem3  19994  ocv1  21609  resttopon  23069  restabs  23073  restopnb  23083  restperf  23092  ordtbas  23100  ordtrest2lem  23111  ordtrest2  23112  leordtvallem1  23118  leordtvallem2  23119  cnclsi  23180  ordtt1  23287  cmpsub  23308  connsub  23329  cnconn  23330  nconnsubb  23331  connsubclo  23332  1stcfb  23353  kgentopon  23446  ptbasfi  23489  ptclsg  23523  dfac14lem  23525  xkoccn  23527  txcnmpt  23532  txtube  23548  xkoptsub  23562  xkopt  23563  kqsat  23639  kqcldsat  23641  ordthmeolem  23709  fbasrn  23792  trfil1  23794  trfil2  23795  trufil  23818  qustgphaus  24031  trust  24137  metustfbas  24465  cfilucfil  24467  xrsmopn  24721  lebnumii  24885  iscmet3  25213  resscdrg  25278  cmmbl  25455  voliunlem3  25473  uniioombllem4  25507  mbflimsup  25587  0plef  25593  0pledm  25594  itg1ge0  25607  mbfi1fseqlem5  25640  itg2addlem  25679  dvcmulf  25868  lhop1  25939  lhop2  25940  efopn  26587  wilthlem2  26999  ex-in  30395  cmcmlem  31561  pjvec  31666  pjocvec  31667  ssmd2  32282  mdslmd4i  32303  chirredlem2  32361  chirredlem3  32362  dmdbr7ati  32394  difuncomp  32523  xppreima  32617  suppovss  32652  fressupp  32659  gtiso  32672  preiman0  32681  fsuppcurry1  32697  fsuppcurry2  32698  resf1o  32703  elrgspnsubrunlem2  33205  elrspunidl  33383  ply1degltdimlem  33625  fldgenfldext  33671  rspectopn  33870  prsss  33919  ordtrestNEW  33924  ordtrest2NEWlem  33925  ordtrest2NEW  33926  lmxrge0  33955  carsggect  34321  probdsb  34425  totprobd  34429  cndprobtot  34439  orvcelval  34472  ballotlemfmpn  34498  signsplypnf  34553  signsply0  34554  dfon2lem4  35799  neibastop3  36375  weiunfrlem  36477  bj-restsnss  37096  bj-ismoored2  37121  bj-inexeqex  37167  bj-idreseq  37175  topdifinfeq  37363  poimirlem3  37642  poimirlem9  37648  mblfinlem3  37678  mblfinlem4  37679  itg2addnclem2  37691  blssp  37775  sstotbnd2  37793  lcvexchlem1  39052  lcvexchlem4  39055  glbconN  39395  pmapglb2N  39789  pmapglb2xN  39790  2polssN  39933  polatN  39949  osumcllem1N  39974  osumcllem9N  39982  pexmidlem6N  39993  diarnN  41147  dihmeetlem11N  41335  dochexmidlem6  41483  lclkrlem2r  41542  mapdunirnN  41668  fsuppssindlem2  42604  prjcrv0  42645  ofoafg  43366  harval3  43550  rfovcnvf1od  44016  fsovcnvlem  44025  ntrneifv3  44094  ntrneifv4  44097  clsneifv3  44122  clsneifv4  44123  neicvgfv  44133  k0004lem2  44160  wnefimgd  44173  inabs3  45072  stoweidlem50  46067  sge0iunmptlemre  46432  caratheodorylem1  46543  smfconst  46766  fresfo  47058  funfocofob  47088  grimuhgr  47897  restclsseplem  48925  incat  49612