Theorem sseqin2 4191

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 3951	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2		incom 4177	. . 3 ⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴)
3	2	eqeq1i 2826	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 ↔ (𝐵 ∩ 𝐴) = 𝐴)
4	1, 3	bitri 277	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∩ 𝐴) = 𝐴)

Syntax hints:   ↔ wb 208   = wceq 1533   ∩ cin 3934   ⊆ wss 3935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1536  df-ex 1777  df-sb 2066  df-clab 2800  df-cleq 2814  df-rab 3147  df-in 3942  df-ss 3951

This theorem is referenced by:  dfss4  4234  rintn0  5022  resabs1  5877  resima2  5882  xpssres  5883  rescnvcnv  6055  sspred  6150  onfr  6224  ordtri2or3  6282  fndmdif  6806  fimacnvinrn2  6835  fveqressseq  6841  sorpssin  7451  predon  7500  omsinds  7594  cnvoprab  7752  frnsuppeq  7836  wfrlem4  7952  fiint  8789  infxpenlem  9433  acndom2  9474  ackbij1lem2  9637  isf34lem5  9794  fpwwe2  10059  uzin  12272  iooval2  12765  fzval2  12889  leiso  13811  fz1isolem  13813  isercolllem3  15017  incexc  15186  bitsinv1  15785  bitsinvp1  15792  bitsshft  15818  dfphi2  16105  ressbas  16548  ressress  16556  ressabs  16557  psssdm  17820  sylow3lem2  18747  gsumxp  19090  dprdsn  19152  ablfac1eu  19189  pgpfac1lem5  19195  ablfaclem3  19203  ocv1  20817  resttopon  21763  restabs  21767  restopnb  21777  restperf  21786  ordtbas  21794  ordtrest2lem  21805  ordtrest2  21806  leordtvallem1  21812  leordtvallem2  21813  cnclsi  21874  ordtt1  21981  cmpsub  22002  connsub  22023  cnconn  22024  nconnsubb  22025  connsubclo  22026  1stcfb  22047  kgentopon  22140  ptbasfi  22183  ptclsg  22217  dfac14lem  22219  xkoccn  22221  txcnmpt  22226  txtube  22242  xkoptsub  22256  xkopt  22257  kqsat  22333  kqcldsat  22335  ordthmeolem  22403  fbasrn  22486  trfil1  22488  trfil2  22489  trufil  22512  qustgphaus  22725  trust  22832  metustfbas  23161  cfilucfil  23163  xrsmopn  23414  lebnumii  23564  iscmet3  23890  resscdrg  23955  cmmbl  24129  voliunlem3  24147  uniioombllem4  24181  mbflimsup  24261  0plef  24267  0pledm  24268  itg1ge0  24281  mbfi1fseqlem5  24314  itg2addlem  24353  dvcmulf  24536  lhop1  24605  lhop2  24606  efopn  25235  wilthlem2  25640  ex-in  28198  cmcmlem  29362  pjvec  29467  pjocvec  29468  ssmd2  30083  mdslmd4i  30104  chirredlem2  30162  chirredlem3  30163  dmdbr7ati  30195  difuncomp  30299  xppreima  30388  suppovss  30420  gtiso  30430  fsuppcurry1  30455  fsuppcurry2  30456  resf1o  30460  prsss  31154  ordtrestNEW  31159  ordtrest2NEWlem  31160  ordtrest2NEW  31161  lmxrge0  31190  carsggect  31571  probdsb  31675  totprobd  31679  cndprobtot  31689  orvcelval  31721  ballotlemfmpn  31747  signsplypnf  31815  signsply0  31816  dfon2lem4  33026  frrlem4  33121  neibastop3  33705  bj-restsnss  34368  bj-ismoored2  34394  bj-inexeqex  34440  bj-idreseq  34448  topdifinfeq  34625  poimirlem3  34889  poimirlem9  34895  mblfinlem3  34925  mblfinlem4  34926  itg2addnclem2  34938  blssp  35025  sstotbnd2  35046  lcvexchlem1  36164  lcvexchlem4  36167  glbconN  36507  pmapglb2N  36901  pmapglb2xN  36902  2polssN  37045  polatN  37061  osumcllem1N  37086  osumcllem9N  37094  pexmidlem6N  37105  diarnN  38259  dihmeetlem11N  38447  dochexmidlem6  38595  lclkrlem2r  38654  mapdunirnN  38780  harval3  39897  rfovcnvf1od  40343  fsovcnvlem  40352  ntrneifv3  40425  ntrneifv4  40428  clsneifv3  40453  clsneifv4  40454  neicvgfv  40464  k0004lem2  40491  wnefimgd  40505  inabs3  41311  mptima2  41510  stoweidlem50  42329  sge0iunmptlemre  42691  caratheodorylem1  42802  smfconst  43020