Theorem sseqin2 4211

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

Syntax hints:   ↔ wb 205   = wceq 1541   ∩ cin 3943   ⊆ wss 3944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-rab 3432  df-in 3951  df-ss 3961

This theorem is referenced by:  dfss4  4254  rintn0  5105  resabs1  6003  resima2  6008  xpssres  6010  rescnvcnv  6192  sspred  6298  trpred  6321  predres  6329  onfr  6392  ordtri2or3  6453  fndmdif  7028  fimacnvinrn2  7059  fveqressseq  7066  sorpssin  7704  predonOLD  7757  omsindsOLD  7860  cnvoprab  8028  frpoins3xpg  8108  frpoins3xp3g  8109  xpord3pred  8120  fsuppeq  8142  fsuppeqg  8143  frrlem4  8256  wfrlem4OLD  8294  fiint  9307  infxpenlem  9990  acndom2  10031  ackbij1lem2  10198  isf34lem5  10355  fpwwe2  10620  uzin  12844  iooval2  13339  fzval2  13469  leiso  14402  fz1isolem  14404  isercolllem3  15595  incexc  15765  bitsinv1  16365  bitsinvp1  16372  bitsshft  16398  dfphi2  16689  ressbas  17161  ressbasOLD  17162  ressress  17175  ressabs  17176  psssdm  18517  sylow3lem2  19460  gsumxp  19803  dprdsn  19865  ablfac1eu  19902  pgpfac1lem5  19908  ablfaclem3  19916  ocv1  21165  resttopon  22594  restabs  22598  restopnb  22608  restperf  22617  ordtbas  22625  ordtrest2lem  22636  ordtrest2  22637  leordtvallem1  22643  leordtvallem2  22644  cnclsi  22705  ordtt1  22812  cmpsub  22833  connsub  22854  cnconn  22855  nconnsubb  22856  connsubclo  22857  1stcfb  22878  kgentopon  22971  ptbasfi  23014  ptclsg  23048  dfac14lem  23050  xkoccn  23052  txcnmpt  23057  txtube  23073  xkoptsub  23087  xkopt  23088  kqsat  23164  kqcldsat  23166  ordthmeolem  23234  fbasrn  23317  trfil1  23319  trfil2  23320  trufil  23343  qustgphaus  23556  trust  23663  metustfbas  23995  cfilucfil  23997  xrsmopn  24257  lebnumii  24411  iscmet3  24739  resscdrg  24804  cmmbl  24980  voliunlem3  24998  uniioombllem4  25032  mbflimsup  25112  0plef  25118  0pledm  25119  itg1ge0  25132  mbfi1fseqlem5  25166  itg2addlem  25205  dvcmulf  25391  lhop1  25460  lhop2  25461  efopn  26095  wilthlem2  26500  ex-in  29543  cmcmlem  30707  pjvec  30812  pjocvec  30813  ssmd2  31428  mdslmd4i  31449  chirredlem2  31507  chirredlem3  31508  dmdbr7ati  31540  difuncomp  31650  xppreima  31740  suppovss  31776  fressupp  31781  gtiso  31793  preiman0  31802  fsuppcurry1  31821  fsuppcurry2  31822  resf1o  31826  elrspunidl  32397  ply1degltdimlem  32543  rspectopn  32676  prsss  32725  ordtrestNEW  32730  ordtrest2NEWlem  32731  ordtrest2NEW  32732  lmxrge0  32761  carsggect  33146  probdsb  33250  totprobd  33254  cndprobtot  33264  orvcelval  33296  ballotlemfmpn  33322  signsplypnf  33390  signsply0  33391  dfon2lem4  34586  neibastop3  35049  bj-restsnss  35766  bj-ismoored2  35791  bj-inexeqex  35837  bj-idreseq  35845  topdifinfeq  36033  poimirlem3  36293  poimirlem9  36299  mblfinlem3  36329  mblfinlem4  36330  itg2addnclem2  36342  blssp  36427  sstotbnd2  36445  lcvexchlem1  37707  lcvexchlem4  37710  glbconN  38050  glbconNOLD  38051  pmapglb2N  38445  pmapglb2xN  38446  2polssN  38589  polatN  38605  osumcllem1N  38630  osumcllem9N  38638  pexmidlem6N  38649  diarnN  39803  dihmeetlem11N  39991  dochexmidlem6  40139  lclkrlem2r  40198  mapdunirnN  40324  fsuppssindlem2  40951  prjcrv0  41155  ofoafg  41873  harval3  42058  rfovcnvf1od  42524  fsovcnvlem  42533  ntrneifv3  42602  ntrneifv4  42605  clsneifv3  42630  clsneifv4  42631  neicvgfv  42641  k0004lem2  42668  wnefimgd  42682  inabs3  43512  mptima2  43720  stoweidlem50  44537  sge0iunmptlemre  44902  caratheodorylem1  45013  smfconst  45236  fresfo  45528  funfocofob  45556  restclsseplem  47193