Theorem sseqin2 4230

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

Syntax hints:   ↔ wb 206   = wceq 1536   ∩ cin 3961   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-in 3969  df-ss 3979

This theorem is referenced by:  dfss4  4274  rintn0  5113  resabs1  6026  resima2  6035  xpssres  6037  mptimass  6092  rescnvcnv  6225  sspred  6331  trpred  6353  predres  6361  onfr  6424  ordtri2or3  6485  fndmdif  7061  fimacnvinrn2  7091  fveqressseq  7098  sorpssin  7749  predonOLD  7805  omsindsOLD  7908  cnvoprab  8083  frpoins3xpg  8163  frpoins3xp3g  8164  xpord3pred  8175  fsuppeq  8198  fsuppeqg  8199  frrlem4  8312  wfrlem4OLD  8350  fiint  9363  fiintOLD  9364  infxpenlem  10050  acndom2  10091  ackbij1lem2  10257  isf34lem5  10415  fpwwe2  10680  uzin  12915  iooval2  13416  fzval2  13546  leiso  14494  fz1isolem  14496  isercolllem3  15699  incexc  15869  bitsinv1  16475  bitsinvp1  16482  bitsshft  16508  dfphi2  16807  ressbas  17279  ressbasOLD  17280  ressress  17293  ressabs  17294  psssdm  18639  sylow3lem2  19660  gsumxp  20008  dprdsn  20070  ablfac1eu  20107  pgpfac1lem5  20113  ablfaclem3  20121  ocv1  21714  resttopon  23184  restabs  23188  restopnb  23198  restperf  23207  ordtbas  23215  ordtrest2lem  23226  ordtrest2  23227  leordtvallem1  23233  leordtvallem2  23234  cnclsi  23295  ordtt1  23402  cmpsub  23423  connsub  23444  cnconn  23445  nconnsubb  23446  connsubclo  23447  1stcfb  23468  kgentopon  23561  ptbasfi  23604  ptclsg  23638  dfac14lem  23640  xkoccn  23642  txcnmpt  23647  txtube  23663  xkoptsub  23677  xkopt  23678  kqsat  23754  kqcldsat  23756  ordthmeolem  23824  fbasrn  23907  trfil1  23909  trfil2  23910  trufil  23933  qustgphaus  24146  trust  24253  metustfbas  24585  cfilucfil  24587  xrsmopn  24847  lebnumii  25011  iscmet3  25340  resscdrg  25405  cmmbl  25582  voliunlem3  25600  uniioombllem4  25634  mbflimsup  25714  0plef  25720  0pledm  25721  itg1ge0  25734  mbfi1fseqlem5  25768  itg2addlem  25807  dvcmulf  25996  lhop1  26067  lhop2  26068  efopn  26714  wilthlem2  27126  ex-in  30453  cmcmlem  31619  pjvec  31724  pjocvec  31725  ssmd2  32340  mdslmd4i  32361  chirredlem2  32419  chirredlem3  32420  dmdbr7ati  32452  difuncomp  32573  xppreima  32661  suppovss  32695  fressupp  32702  gtiso  32715  preiman0  32724  fsuppcurry1  32742  fsuppcurry2  32743  resf1o  32747  elrspunidl  33435  ply1degltdimlem  33649  fldgenfldext  33692  rspectopn  33827  prsss  33876  ordtrestNEW  33881  ordtrest2NEWlem  33882  ordtrest2NEW  33883  lmxrge0  33912  carsggect  34299  probdsb  34403  totprobd  34407  cndprobtot  34417  orvcelval  34449  ballotlemfmpn  34475  signsplypnf  34543  signsply0  34544  dfon2lem4  35767  neibastop3  36344  weiunfrlem  36446  bj-restsnss  37065  bj-ismoored2  37090  bj-inexeqex  37136  bj-idreseq  37144  topdifinfeq  37332  poimirlem3  37609  poimirlem9  37615  mblfinlem3  37645  mblfinlem4  37646  itg2addnclem2  37658  blssp  37742  sstotbnd2  37760  lcvexchlem1  39015  lcvexchlem4  39018  glbconN  39358  glbconNOLD  39359  pmapglb2N  39753  pmapglb2xN  39754  2polssN  39897  polatN  39913  osumcllem1N  39938  osumcllem9N  39946  pexmidlem6N  39957  diarnN  41111  dihmeetlem11N  41299  dochexmidlem6  41447  lclkrlem2r  41506  mapdunirnN  41632  fsuppssindlem2  42578  prjcrv0  42619  ofoafg  43343  harval3  43527  rfovcnvf1od  43993  fsovcnvlem  44002  ntrneifv3  44071  ntrneifv4  44074  clsneifv3  44099  clsneifv4  44100  neicvgfv  44110  k0004lem2  44137  wnefimgd  44150  inabs3  44995  stoweidlem50  46005  sge0iunmptlemre  46370  caratheodorylem1  46481  smfconst  46704  fresfo  46997  funfocofob  47027  grimuhgr  47815  restclsseplem  48710