Theorem sseqin2 4149

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 3904	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2		incom 4135	. . 3 ⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴)
3	2	eqeq1i 2743	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 ↔ (𝐵 ∩ 𝐴) = 𝐴)
4	1, 3	bitri 274	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∩ 𝐴) = 𝐴)

Syntax hints:   ↔ wb 205   = wceq 1539   ∩ cin 3886   ⊆ wss 3887

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-rab 3073  df-in 3894  df-ss 3904

This theorem is referenced by:  dfss4  4192  rintn0  5038  resabs1  5921  resima2  5926  xpssres  5928  rescnvcnv  6107  sspred  6211  trpred  6234  predres  6242  onfr  6305  ordtri2or3  6363  fndmdif  6919  fimacnvinrn2  6950  fveqressseq  6957  sorpssin  7584  predonOLD  7636  omsindsOLD  7734  cnvoprab  7900  frnsuppeq  7991  frnsuppeqg  7992  frrlem4  8105  wfrlem4OLD  8143  fiint  9091  infxpenlem  9769  acndom2  9810  ackbij1lem2  9977  isf34lem5  10134  fpwwe2  10399  uzin  12618  iooval2  13112  fzval2  13242  leiso  14173  fz1isolem  14175  isercolllem3  15378  incexc  15549  bitsinv1  16149  bitsinvp1  16156  bitsshft  16182  dfphi2  16475  ressbas  16947  ressbasOLD  16948  ressress  16958  ressabs  16959  psssdm  18300  sylow3lem2  19233  gsumxp  19577  dprdsn  19639  ablfac1eu  19676  pgpfac1lem5  19682  ablfaclem3  19690  ocv1  20884  resttopon  22312  restabs  22316  restopnb  22326  restperf  22335  ordtbas  22343  ordtrest2lem  22354  ordtrest2  22355  leordtvallem1  22361  leordtvallem2  22362  cnclsi  22423  ordtt1  22530  cmpsub  22551  connsub  22572  cnconn  22573  nconnsubb  22574  connsubclo  22575  1stcfb  22596  kgentopon  22689  ptbasfi  22732  ptclsg  22766  dfac14lem  22768  xkoccn  22770  txcnmpt  22775  txtube  22791  xkoptsub  22805  xkopt  22806  kqsat  22882  kqcldsat  22884  ordthmeolem  22952  fbasrn  23035  trfil1  23037  trfil2  23038  trufil  23061  qustgphaus  23274  trust  23381  metustfbas  23713  cfilucfil  23715  xrsmopn  23975  lebnumii  24129  iscmet3  24457  resscdrg  24522  cmmbl  24698  voliunlem3  24716  uniioombllem4  24750  mbflimsup  24830  0plef  24836  0pledm  24837  itg1ge0  24850  mbfi1fseqlem5  24884  itg2addlem  24923  dvcmulf  25109  lhop1  25178  lhop2  25179  efopn  25813  wilthlem2  26218  ex-in  28789  cmcmlem  29953  pjvec  30058  pjocvec  30059  ssmd2  30674  mdslmd4i  30695  chirredlem2  30753  chirredlem3  30754  dmdbr7ati  30786  difuncomp  30893  xppreima  30983  suppovss  31017  fressupp  31022  gtiso  31033  preiman0  31042  fsuppcurry1  31060  fsuppcurry2  31061  resf1o  31065  elrspunidl  31606  rspectopn  31817  prsss  31866  ordtrestNEW  31871  ordtrest2NEWlem  31872  ordtrest2NEW  31873  lmxrge0  31902  carsggect  32285  probdsb  32389  totprobd  32393  cndprobtot  32403  orvcelval  32435  ballotlemfmpn  32461  signsplypnf  32529  signsply0  32530  dfon2lem4  33762  frpoins3xpg  33787  frpoins3xp3g  33788  xpord3pred  33798  neibastop3  34551  bj-restsnss  35254  bj-ismoored2  35279  bj-inexeqex  35325  bj-idreseq  35333  topdifinfeq  35521  poimirlem3  35780  poimirlem9  35786  mblfinlem3  35816  mblfinlem4  35817  itg2addnclem2  35829  blssp  35914  sstotbnd2  35932  lcvexchlem1  37048  lcvexchlem4  37051  glbconN  37391  pmapglb2N  37785  pmapglb2xN  37786  2polssN  37929  polatN  37945  osumcllem1N  37970  osumcllem9N  37978  pexmidlem6N  37989  diarnN  39143  dihmeetlem11N  39331  dochexmidlem6  39479  lclkrlem2r  39538  mapdunirnN  39664  fsuppssindlem2  40281  harval3  41145  rfovcnvf1od  41612  fsovcnvlem  41621  ntrneifv3  41692  ntrneifv4  41695  clsneifv3  41720  clsneifv4  41721  neicvgfv  41731  k0004lem2  41758  wnefimgd  41772  inabs3  42604  mptima2  42791  stoweidlem50  43591  sge0iunmptlemre  43953  caratheodorylem1  44064  smfconst  44285  fresfo  44542  funfocofob  44570  restclsseplem  46208