Theorem sseqin2 4159

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

Syntax hints:   ↔ wb 207   = wceq 1547   ∩ cin 3889   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1094  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-in 3897  df-ss 3907

This theorem is referenced by:  dfss4  4204  rintn0  5045  resabs1  5965  resima2  5975  xpssres  5977  mptimass  6032  rescnvcnv  6162  sspred  6268  trpred  6289  predres  6297  onfr  6356  ordtri2or3  6419  fndmdif  6990  fimacnvinrn2  7020  fveqressseq  7027  sorpssin  7681  cnvoprab  8009  frpoins3xpg  8087  frpoins3xp3g  8088  xpord3pred  8099  fsuppeq  8122  fsuppeqg  8123  frrlem4  8236  fiint  9234  infxpenlem  9933  acndom2  9974  ackbij1lem2  10140  isf34lem5  10298  fpwwe2  10564  uzin  12822  iooval2  13329  fzval2  13462  leiso  14419  fz1isolem  14421  isercolllem3  15627  incexc  15800  bitsinv1  16409  bitsinvp1  16416  bitsshft  16442  dfphi2  16742  ressbas  17204  ressress  17215  ressabs  17216  psssdm  18546  sylow3lem2  19601  gsumxp  19949  dprdsn  20011  ablfac1eu  20048  pgpfac1lem5  20054  ablfaclem3  20062  ocv1  21661  resttopon  23151  restabs  23155  restopnb  23165  restperf  23174  ordtbas  23182  ordtrest2lem  23193  ordtrest2  23194  leordtvallem1  23200  leordtvallem2  23201  cnclsi  23262  ordtt1  23369  cmpsub  23390  connsub  23411  cnconn  23412  nconnsubb  23413  connsubclo  23414  1stcfb  23435  kgentopon  23528  ptbasfi  23571  ptclsg  23605  dfac14lem  23607  xkoccn  23609  txcnmpt  23614  txtube  23630  xkoptsub  23644  xkopt  23645  kqsat  23721  kqcldsat  23723  ordthmeolem  23791  fbasrn  23874  trfil1  23876  trfil2  23877  trufil  23900  qustgphaus  24113  trust  24219  metustfbas  24547  cfilucfil  24549  xrsmopn  24803  lebnumii  24958  iscmet3  25285  resscdrg  25350  cmmbl  25526  voliunlem3  25544  uniioombllem4  25578  mbflimsup  25658  0plef  25664  0pledm  25665  itg1ge0  25678  mbfi1fseqlem5  25711  itg2addlem  25750  dvcmulf  25937  lhop1  26006  lhop2  26007  efopn  26647  wilthlem2  27057  ex-in  30520  cmcmlem  31687  pjvec  31792  pjocvec  31793  ssmd2  32408  mdslmd4i  32429  chirredlem2  32487  chirredlem3  32488  dmdbr7ati  32520  difuncomp  32649  xppreima  32744  partfun2  32775  suppovss  32780  fressupp  32787  gtiso  32800  preiman0  32809  fsuppcurry1  32823  fsuppcurry2  32824  resf1o  32829  elrgspnsubrunlem2  33336  elrspunidl  33518  ply1degltdimlem  33813  fldgenfldext  33859  rspectopn  34058  prsss  34107  ordtrestNEW  34112  ordtrest2NEWlem  34113  ordtrest2NEW  34114  lmxrge0  34143  carsggect  34509  probdsb  34613  totprobd  34617  cndprobtot  34627  orvcelval  34660  ballotlemfmpn  34686  signsplypnf  34741  signsply0  34742  dfon2lem4  36013  neibastop3  36591  weiunfrlem  36693  bj-restsnss  37442  bj-ismoored2  37467  bj-inexeqex  37515  bj-idreseq  37523  topdifinfeq  37713  poimirlem3  37991  poimirlem9  37997  mblfinlem3  38027  mblfinlem4  38028  itg2addnclem2  38040  blssp  38124  sstotbnd2  38142  lcvexchlem1  39527  lcvexchlem4  39530  glbconN  39870  pmapglb2N  40264  pmapglb2xN  40265  2polssN  40408  polatN  40424  osumcllem1N  40449  osumcllem9N  40457  pexmidlem6N  40468  diarnN  41622  dihmeetlem11N  41810  dochexmidlem6  41958  lclkrlem2r  42017  mapdunirnN  42143  fsuppssindlem2  43043  prjcrv0  43084  ofoafg  43800  harval3  43983  rfovcnvf1od  44449  fsovcnvlem  44458  ntrneifv3  44527  ntrneifv4  44530  clsneifv3  44555  clsneifv4  44556  neicvgfv  44566  k0004lem2  44593  wnefimgd  44606  inabs3  45505  stoweidlem50  46494  sge0iunmptlemre  46859  caratheodorylem1  46970  smfconst  47193  fresfo  47512  funfocofob  47542  grimuhgr  48379  restclsseplem  49406  incat  50092