Theorem sseqin2 4176

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

Syntax hints:   ↔ wb 206   = wceq 1542   ∩ cin 3901   ⊆ wss 3902

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 3401  df-in 3909  df-ss 3919

This theorem is referenced by:  dfss4  4222  rintn0  5065  resabs1  5966  resima2  5976  xpssres  5978  mptimass  6033  rescnvcnv  6163  sspred  6269  trpred  6290  predres  6298  onfr  6357  ordtri2or3  6420  fndmdif  6989  fimacnvinrn2  7019  fveqressseq  7026  sorpssin  7678  cnvoprab  8006  frpoins3xpg  8084  frpoins3xp3g  8085  xpord3pred  8096  fsuppeq  8119  fsuppeqg  8120  frrlem4  8233  fiint  9231  infxpenlem  9927  acndom2  9968  ackbij1lem2  10134  isf34lem5  10292  fpwwe2  10558  uzin  12791  iooval2  13298  fzval2  13430  leiso  14386  fz1isolem  14388  isercolllem3  15594  incexc  15764  bitsinv1  16373  bitsinvp1  16380  bitsshft  16406  dfphi2  16705  ressbas  17167  ressress  17178  ressabs  17179  psssdm  18509  sylow3lem2  19561  gsumxp  19909  dprdsn  19971  ablfac1eu  20008  pgpfac1lem5  20014  ablfaclem3  20022  ocv1  21638  resttopon  23109  restabs  23113  restopnb  23123  restperf  23132  ordtbas  23140  ordtrest2lem  23151  ordtrest2  23152  leordtvallem1  23158  leordtvallem2  23159  cnclsi  23220  ordtt1  23327  cmpsub  23348  connsub  23369  cnconn  23370  nconnsubb  23371  connsubclo  23372  1stcfb  23393  kgentopon  23486  ptbasfi  23529  ptclsg  23563  dfac14lem  23565  xkoccn  23567  txcnmpt  23572  txtube  23588  xkoptsub  23602  xkopt  23603  kqsat  23679  kqcldsat  23681  ordthmeolem  23749  fbasrn  23832  trfil1  23834  trfil2  23835  trufil  23858  qustgphaus  24071  trust  24177  metustfbas  24505  cfilucfil  24507  xrsmopn  24761  lebnumii  24925  iscmet3  25253  resscdrg  25318  cmmbl  25495  voliunlem3  25513  uniioombllem4  25547  mbflimsup  25627  0plef  25633  0pledm  25634  itg1ge0  25647  mbfi1fseqlem5  25680  itg2addlem  25719  dvcmulf  25908  lhop1  25979  lhop2  25980  efopn  26627  wilthlem2  27039  ex-in  30483  cmcmlem  31649  pjvec  31754  pjocvec  31755  ssmd2  32370  mdslmd4i  32391  chirredlem2  32449  chirredlem3  32450  dmdbr7ati  32482  difuncomp  32610  xppreima  32705  partfun2  32736  suppovss  32741  fressupp  32748  gtiso  32761  preiman0  32770  fsuppcurry1  32784  fsuppcurry2  32785  resf1o  32790  elrgspnsubrunlem2  33311  elrspunidl  33490  ply1degltdimlem  33760  fldgenfldext  33806  rspectopn  34005  prsss  34054  ordtrestNEW  34059  ordtrest2NEWlem  34060  ordtrest2NEW  34061  lmxrge0  34090  carsggect  34456  probdsb  34560  totprobd  34564  cndprobtot  34574  orvcelval  34607  ballotlemfmpn  34633  signsplypnf  34688  signsply0  34689  dfon2lem4  35959  neibastop3  36537  weiunfrlem  36639  bj-restsnss  37259  bj-ismoored2  37284  bj-inexeqex  37330  bj-idreseq  37338  topdifinfeq  37526  poimirlem3  37795  poimirlem9  37801  mblfinlem3  37831  mblfinlem4  37832  itg2addnclem2  37844  blssp  37928  sstotbnd2  37946  lcvexchlem1  39331  lcvexchlem4  39334  glbconN  39674  pmapglb2N  40068  pmapglb2xN  40069  2polssN  40212  polatN  40228  osumcllem1N  40253  osumcllem9N  40261  pexmidlem6N  40272  diarnN  41426  dihmeetlem11N  41614  dochexmidlem6  41762  lclkrlem2r  41821  mapdunirnN  41947  fsuppssindlem2  42871  prjcrv0  42912  ofoafg  43632  harval3  43815  rfovcnvf1od  44281  fsovcnvlem  44290  ntrneifv3  44359  ntrneifv4  44362  clsneifv3  44387  clsneifv4  44388  neicvgfv  44398  k0004lem2  44425  wnefimgd  44438  inabs3  45337  stoweidlem50  46330  sge0iunmptlemre  46695  caratheodorylem1  46806  smfconst  47029  fresfo  47330  funfocofob  47360  grimuhgr  48169  restclsseplem  49196  incat  49882