Theorem sseqin2 4216

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

Syntax hints:   ↔ wb 205   = wceq 1542   ∩ cin 3948   ⊆ wss 3949

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 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-rab 3434  df-in 3956  df-ss 3966

This theorem is referenced by:  dfss4  4259  rintn0  5113  resabs1  6012  resima2  6017  xpssres  6019  mptimass  6073  rescnvcnv  6204  sspred  6310  trpred  6333  predres  6341  onfr  6404  ordtri2or3  6465  fndmdif  7044  fimacnvinrn2  7075  fveqressseq  7082  sorpssin  7721  predonOLD  7774  omsindsOLD  7877  cnvoprab  8046  frpoins3xpg  8126  frpoins3xp3g  8127  xpord3pred  8138  fsuppeq  8160  fsuppeqg  8161  frrlem4  8274  wfrlem4OLD  8312  fiint  9324  infxpenlem  10008  acndom2  10049  ackbij1lem2  10216  isf34lem5  10373  fpwwe2  10638  uzin  12862  iooval2  13357  fzval2  13487  leiso  14420  fz1isolem  14422  isercolllem3  15613  incexc  15783  bitsinv1  16383  bitsinvp1  16390  bitsshft  16416  dfphi2  16707  ressbas  17179  ressbasOLD  17180  ressress  17193  ressabs  17194  psssdm  18535  sylow3lem2  19496  gsumxp  19844  dprdsn  19906  ablfac1eu  19943  pgpfac1lem5  19949  ablfaclem3  19957  ocv1  21232  resttopon  22665  restabs  22669  restopnb  22679  restperf  22688  ordtbas  22696  ordtrest2lem  22707  ordtrest2  22708  leordtvallem1  22714  leordtvallem2  22715  cnclsi  22776  ordtt1  22883  cmpsub  22904  connsub  22925  cnconn  22926  nconnsubb  22927  connsubclo  22928  1stcfb  22949  kgentopon  23042  ptbasfi  23085  ptclsg  23119  dfac14lem  23121  xkoccn  23123  txcnmpt  23128  txtube  23144  xkoptsub  23158  xkopt  23159  kqsat  23235  kqcldsat  23237  ordthmeolem  23305  fbasrn  23388  trfil1  23390  trfil2  23391  trufil  23414  qustgphaus  23627  trust  23734  metustfbas  24066  cfilucfil  24068  xrsmopn  24328  lebnumii  24482  iscmet3  24810  resscdrg  24875  cmmbl  25051  voliunlem3  25069  uniioombllem4  25103  mbflimsup  25183  0plef  25189  0pledm  25190  itg1ge0  25203  mbfi1fseqlem5  25237  itg2addlem  25276  dvcmulf  25462  lhop1  25531  lhop2  25532  efopn  26166  wilthlem2  26573  ex-in  29678  cmcmlem  30844  pjvec  30949  pjocvec  30950  ssmd2  31565  mdslmd4i  31586  chirredlem2  31644  chirredlem3  31645  dmdbr7ati  31677  difuncomp  31785  xppreima  31871  suppovss  31906  fressupp  31910  gtiso  31922  preiman0  31931  fsuppcurry1  31950  fsuppcurry2  31951  resf1o  31955  elrspunidl  32546  ply1degltdimlem  32707  rspectopn  32847  prsss  32896  ordtrestNEW  32901  ordtrest2NEWlem  32902  ordtrest2NEW  32903  lmxrge0  32932  carsggect  33317  probdsb  33421  totprobd  33425  cndprobtot  33435  orvcelval  33467  ballotlemfmpn  33493  signsplypnf  33561  signsply0  33562  dfon2lem4  34758  neibastop3  35247  bj-restsnss  35964  bj-ismoored2  35989  bj-inexeqex  36035  bj-idreseq  36043  topdifinfeq  36231  poimirlem3  36491  poimirlem9  36497  mblfinlem3  36527  mblfinlem4  36528  itg2addnclem2  36540  blssp  36624  sstotbnd2  36642  lcvexchlem1  37904  lcvexchlem4  37907  glbconN  38247  glbconNOLD  38248  pmapglb2N  38642  pmapglb2xN  38643  2polssN  38786  polatN  38802  osumcllem1N  38827  osumcllem9N  38835  pexmidlem6N  38846  diarnN  40000  dihmeetlem11N  40188  dochexmidlem6  40336  lclkrlem2r  40395  mapdunirnN  40521  fsuppssindlem2  41164  prjcrv0  41375  ofoafg  42104  harval3  42289  rfovcnvf1od  42755  fsovcnvlem  42764  ntrneifv3  42833  ntrneifv4  42836  clsneifv3  42861  clsneifv4  42862  neicvgfv  42872  k0004lem2  42899  wnefimgd  42913  inabs3  43743  stoweidlem50  44766  sge0iunmptlemre  45131  caratheodorylem1  45242  smfconst  45465  fresfo  45758  funfocofob  45786  restclsseplem  47547