Theorem sseqin2 4164

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

Syntax hints:   ↔ wb 206   = wceq 1542   ∩ cin 3889   ⊆ wss 3890

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-in 3897  df-ss 3907

This theorem is referenced by:  dfss4  4210  rintn0  5052  resabs1  5963  resima2  5973  xpssres  5975  mptimass  6030  rescnvcnv  6160  sspred  6266  trpred  6287  predres  6295  onfr  6354  ordtri2or3  6417  fndmdif  6986  fimacnvinrn2  7016  fveqressseq  7023  sorpssin  7676  cnvoprab  8004  frpoins3xpg  8081  frpoins3xp3g  8082  xpord3pred  8093  fsuppeq  8116  fsuppeqg  8117  frrlem4  8230  fiint  9228  infxpenlem  9924  acndom2  9965  ackbij1lem2  10131  isf34lem5  10289  fpwwe2  10555  uzin  12813  iooval2  13320  fzval2  13453  leiso  14410  fz1isolem  14412  isercolllem3  15618  incexc  15791  bitsinv1  16400  bitsinvp1  16407  bitsshft  16433  dfphi2  16733  ressbas  17195  ressress  17206  ressabs  17207  psssdm  18537  sylow3lem2  19592  gsumxp  19940  dprdsn  20002  ablfac1eu  20039  pgpfac1lem5  20045  ablfaclem3  20053  ocv1  21667  resttopon  23135  restabs  23139  restopnb  23149  restperf  23158  ordtbas  23166  ordtrest2lem  23177  ordtrest2  23178  leordtvallem1  23184  leordtvallem2  23185  cnclsi  23246  ordtt1  23353  cmpsub  23374  connsub  23395  cnconn  23396  nconnsubb  23397  connsubclo  23398  1stcfb  23419  kgentopon  23512  ptbasfi  23555  ptclsg  23589  dfac14lem  23591  xkoccn  23593  txcnmpt  23598  txtube  23614  xkoptsub  23628  xkopt  23629  kqsat  23705  kqcldsat  23707  ordthmeolem  23775  fbasrn  23858  trfil1  23860  trfil2  23861  trufil  23884  qustgphaus  24097  trust  24203  metustfbas  24531  cfilucfil  24533  xrsmopn  24787  lebnumii  24942  iscmet3  25269  resscdrg  25334  cmmbl  25510  voliunlem3  25528  uniioombllem4  25562  mbflimsup  25642  0plef  25648  0pledm  25649  itg1ge0  25662  mbfi1fseqlem5  25695  itg2addlem  25734  dvcmulf  25921  lhop1  25991  lhop2  25992  efopn  26638  wilthlem2  27050  ex-in  30515  cmcmlem  31682  pjvec  31787  pjocvec  31788  ssmd2  32403  mdslmd4i  32424  chirredlem2  32482  chirredlem3  32483  dmdbr7ati  32515  difuncomp  32643  xppreima  32738  partfun2  32769  suppovss  32774  fressupp  32781  gtiso  32794  preiman0  32803  fsuppcurry1  32817  fsuppcurry2  32818  resf1o  32823  elrgspnsubrunlem2  33329  elrspunidl  33508  ply1degltdimlem  33787  fldgenfldext  33833  rspectopn  34032  prsss  34081  ordtrestNEW  34086  ordtrest2NEWlem  34087  ordtrest2NEW  34088  lmxrge0  34117  carsggect  34483  probdsb  34587  totprobd  34591  cndprobtot  34601  orvcelval  34634  ballotlemfmpn  34660  signsplypnf  34715  signsply0  34716  dfon2lem4  35987  neibastop3  36565  weiunfrlem  36667  bj-restsnss  37408  bj-ismoored2  37433  bj-inexeqex  37481  bj-idreseq  37489  topdifinfeq  37677  poimirlem3  37955  poimirlem9  37961  mblfinlem3  37991  mblfinlem4  37992  itg2addnclem2  38004  blssp  38088  sstotbnd2  38106  lcvexchlem1  39491  lcvexchlem4  39494  glbconN  39834  pmapglb2N  40228  pmapglb2xN  40229  2polssN  40372  polatN  40388  osumcllem1N  40413  osumcllem9N  40421  pexmidlem6N  40432  diarnN  41586  dihmeetlem11N  41774  dochexmidlem6  41922  lclkrlem2r  41981  mapdunirnN  42107  fsuppssindlem2  43036  prjcrv0  43077  ofoafg  43797  harval3  43980  rfovcnvf1od  44446  fsovcnvlem  44455  ntrneifv3  44524  ntrneifv4  44527  clsneifv3  44552  clsneifv4  44553  neicvgfv  44563  k0004lem2  44590  wnefimgd  44603  inabs3  45502  stoweidlem50  46493  sge0iunmptlemre  46858  caratheodorylem1  46969  smfconst  47192  fresfo  47493  funfocofob  47523  grimuhgr  48360  restclsseplem  49387  incat  50073