Theorem sseqin2 4189

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∩ cin 3916   ⊆ wss 3917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-in 3924  df-ss 3934

This theorem is referenced by:  dfss4  4235  rintn0  5076  resabs1  5980  resima2  5990  xpssres  5992  mptimass  6047  rescnvcnv  6180  sspred  6286  trpred  6307  predres  6315  onfr  6374  ordtri2or3  6437  fndmdif  7017  fimacnvinrn2  7047  fveqressseq  7054  sorpssin  7710  cnvoprab  8042  frpoins3xpg  8122  frpoins3xp3g  8123  xpord3pred  8134  fsuppeq  8157  fsuppeqg  8158  frrlem4  8271  fiint  9284  fiintOLD  9285  infxpenlem  9973  acndom2  10014  ackbij1lem2  10180  isf34lem5  10338  fpwwe2  10603  uzin  12840  iooval2  13346  fzval2  13478  leiso  14431  fz1isolem  14433  isercolllem3  15640  incexc  15810  bitsinv1  16419  bitsinvp1  16426  bitsshft  16452  dfphi2  16751  ressbas  17213  ressress  17224  ressabs  17225  psssdm  18548  sylow3lem2  19565  gsumxp  19913  dprdsn  19975  ablfac1eu  20012  pgpfac1lem5  20018  ablfaclem3  20026  ocv1  21595  resttopon  23055  restabs  23059  restopnb  23069  restperf  23078  ordtbas  23086  ordtrest2lem  23097  ordtrest2  23098  leordtvallem1  23104  leordtvallem2  23105  cnclsi  23166  ordtt1  23273  cmpsub  23294  connsub  23315  cnconn  23316  nconnsubb  23317  connsubclo  23318  1stcfb  23339  kgentopon  23432  ptbasfi  23475  ptclsg  23509  dfac14lem  23511  xkoccn  23513  txcnmpt  23518  txtube  23534  xkoptsub  23548  xkopt  23549  kqsat  23625  kqcldsat  23627  ordthmeolem  23695  fbasrn  23778  trfil1  23780  trfil2  23781  trufil  23804  qustgphaus  24017  trust  24124  metustfbas  24452  cfilucfil  24454  xrsmopn  24708  lebnumii  24872  iscmet3  25200  resscdrg  25265  cmmbl  25442  voliunlem3  25460  uniioombllem4  25494  mbflimsup  25574  0plef  25580  0pledm  25581  itg1ge0  25594  mbfi1fseqlem5  25627  itg2addlem  25666  dvcmulf  25855  lhop1  25926  lhop2  25927  efopn  26574  wilthlem2  26986  ex-in  30361  cmcmlem  31527  pjvec  31632  pjocvec  31633  ssmd2  32248  mdslmd4i  32269  chirredlem2  32327  chirredlem3  32328  dmdbr7ati  32360  difuncomp  32489  xppreima  32576  suppovss  32611  fressupp  32618  gtiso  32631  preiman0  32640  fsuppcurry1  32655  fsuppcurry2  32656  resf1o  32660  elrgspnsubrunlem2  33206  elrspunidl  33406  ply1degltdimlem  33625  fldgenfldext  33670  rspectopn  33864  prsss  33913  ordtrestNEW  33918  ordtrest2NEWlem  33919  ordtrest2NEW  33920  lmxrge0  33949  carsggect  34316  probdsb  34420  totprobd  34424  cndprobtot  34434  orvcelval  34467  ballotlemfmpn  34493  signsplypnf  34548  signsply0  34549  dfon2lem4  35781  neibastop3  36357  weiunfrlem  36459  bj-restsnss  37078  bj-ismoored2  37103  bj-inexeqex  37149  bj-idreseq  37157  topdifinfeq  37345  poimirlem3  37624  poimirlem9  37630  mblfinlem3  37660  mblfinlem4  37661  itg2addnclem2  37673  blssp  37757  sstotbnd2  37775  lcvexchlem1  39034  lcvexchlem4  39037  glbconN  39377  glbconNOLD  39378  pmapglb2N  39772  pmapglb2xN  39773  2polssN  39916  polatN  39932  osumcllem1N  39957  osumcllem9N  39965  pexmidlem6N  39976  diarnN  41130  dihmeetlem11N  41318  dochexmidlem6  41466  lclkrlem2r  41525  mapdunirnN  41651  fsuppssindlem2  42587  prjcrv0  42628  ofoafg  43350  harval3  43534  rfovcnvf1od  44000  fsovcnvlem  44009  ntrneifv3  44078  ntrneifv4  44081  clsneifv3  44106  clsneifv4  44107  neicvgfv  44117  k0004lem2  44144  wnefimgd  44157  inabs3  45057  stoweidlem50  46055  sge0iunmptlemre  46420  caratheodorylem1  46531  smfconst  46754  fresfo  47053  funfocofob  47083  grimuhgr  47891  restclsseplem  48907  incat  49594