Theorem sseqin2 4178

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 3925	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2		ineqcom 4165	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 ↔ (𝐵 ∩ 𝐴) = 𝐴)
3	1, 2	bitri 278	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∩ 𝐴) = 𝐴)

Syntax hints:   ↔ wb 209   = wceq 1563   ∩ cin 3906   ⊆ wss 3907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-in 3914  df-ss 3924

This theorem is referenced by:  dfss4  4224  rintn0  5071  resabs1  5996  resima2  6006  xpssres  6008  mptimass  6066  rescnvcnv  6195  sspred  6301  trpred  6322  predres  6330  onfr  6389  ordtri2or3  6452  fndmdif  7027  fimacnvinrn2  7057  fveqressseq  7064  sorpssin  7718  cnvoprab  8045  frpoins3xpg  8124  frpoins3xp3g  8125  xpord3pred  8136  fsuppeq  8159  fsuppeqg  8160  frrlem4  8274  fiint  9274  infxpenlem  9985  acndom2  10026  ackbij1lem2  10191  isf34lem5  10350  fpwwe2  10616  uzin  12889  iooval2  13396  fzval2  13529  leiso  14486  fz1isolem  14488  isercolllem3  15708  incexc  15881  bitsinv1  16490  bitsinvp1  16497  bitsshft  16523  dfphi2  16823  ressbas  17286  ressress  17297  ressabs  17298  psssdm  18628  sylow3lem2  19689  gsumxp  20037  dprdsn  20099  ablfac1eu  20136  pgpfac1lem5  20142  ablfaclem3  20150  ocv1  21789  resttopon  23279  restabs  23283  restopnb  23293  restperf  23302  ordtbas  23310  ordtrest2lem  23321  ordtrest2  23322  leordtvallem1  23328  leordtvallem2  23329  cnclsi  23390  ordtt1  23497  cmpsub  23518  connsub  23539  cnconn  23540  nconnsubb  23541  connsubclo  23542  1stcfb  23563  kgentopon  23656  ptbasfi  23699  ptclsg  23733  dfac14lem  23735  xkoccn  23737  txcnmpt  23742  txtube  23758  xkoptsub  23772  xkopt  23773  kqsat  23849  kqcldsat  23851  ordthmeolem  23919  fbasrn  24002  trfil1  24004  trfil2  24005  trufil  24028  qustgphaus  24241  trust  24347  metustfbas  24675  cfilucfil  24677  xrsmopn  24931  lebnumii  25086  iscmet3  25413  resscdrg  25478  cmmbl  25654  voliunlem3  25672  uniioombllem4  25706  mbflimsup  25786  0plef  25792  0pledm  25793  itg1ge0  25806  mbfi1fseqlem5  25839  itg2addlem  25878  dvcmulf  26065  lhop1  26134  lhop2  26135  efopn  26781  wilthlem2  27191  ex-in  30685  cmcmlem  31852  pjvec  31957  pjocvec  31958  ssmd2  32573  mdslmd4i  32594  chirredlem2  32652  chirredlem3  32653  dmdbr7ati  32685  difuncomp  32808  xppreima  32902  partfun2  32933  suppovss  32938  fressupp  32945  gtiso  32958  preiman0  32967  fsuppcurry1  32981  fsuppcurry2  32982  resf1o  32987  elrgspnsubrunlem2  33481  elrspunidl  33652  ply1degltdimlem  33929  fldgenfldext  33975  rspectopn  34174  prsss  34223  ordtrestNEW  34228  ordtrest2NEWlem  34229  ordtrest2NEW  34230  lmxrge0  34259  carsggect  34625  probdsb  34729  totprobd  34733  cndprobtot  34743  orvcelval  34776  ballotlemfmpn  34802  signsplypnf  34854  signsply0  34855  dfon2lem4  36147  neibastop3  36735  weiunfrlem  36837  bj-restsnss  37585  bj-ismoored2  37610  bj-inexeqex  37658  bj-idreseq  37666  topdifinfeq  37856  poimirlem3  38134  poimirlem9  38140  mblfinlem3  38170  mblfinlem4  38171  itg2addnclem2  38183  blssp  38267  sstotbnd2  38285  lcvexchlem1  39670  lcvexchlem4  39673  glbconN  40013  pmapglb2N  40407  pmapglb2xN  40408  2polssN  40551  polatN  40567  osumcllem1N  40592  osumcllem9N  40600  pexmidlem6N  40611  diarnN  41765  dihmeetlem11N  41953  dochexmidlem6  42101  lclkrlem2r  42160  mapdunirnN  42286  fsuppssindlem2  43186  prjcrv0  43227  ofoafg  43943  harval3  44126  rfovcnvf1od  44592  fsovcnvlem  44601  ntrneifv3  44670  ntrneifv4  44673  clsneifv3  44698  clsneifv4  44699  neicvgfv  44709  k0004lem2  44736  wnefimgd  44749  inabs3  45634  stoweidlem50  46622  sge0iunmptlemre  46987  caratheodorylem1  47098  smfconst  47321  fresfo  47640  funfocofob  47670  grimuhgr  48507  restclsseplem  49544  incat  50230