Theorem sseqin2 4216

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

Syntax hints:   ↔ wb 205   = wceq 1542   ∩ cin 3948   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-rab 3434  df-in 3956  df-ss 3966

This theorem is referenced by:  dfss4  4259  rintn0  5113  resabs1  6012  resima2  6017  xpssres  6019  mptimass  6073  rescnvcnv  6204  sspred  6310  trpred  6333  predres  6341  onfr  6404  ordtri2or3  6465  fndmdif  7044  fimacnvinrn2  7075  fveqressseq  7082  sorpssin  7721  predonOLD  7774  omsindsOLD  7877  cnvoprab  8046  frpoins3xpg  8126  frpoins3xp3g  8127  xpord3pred  8138  fsuppeq  8160  fsuppeqg  8161  frrlem4  8274  wfrlem4OLD  8312  fiint  9324  infxpenlem  10008  acndom2  10049  ackbij1lem2  10216  isf34lem5  10373  fpwwe2  10638  uzin  12862  iooval2  13357  fzval2  13487  leiso  14420  fz1isolem  14422  isercolllem3  15613  incexc  15783  bitsinv1  16383  bitsinvp1  16390  bitsshft  16416  dfphi2  16707  ressbas  17179  ressbasOLD  17180  ressress  17193  ressabs  17194  psssdm  18535  sylow3lem2  19496  gsumxp  19844  dprdsn  19906  ablfac1eu  19943  pgpfac1lem5  19949  ablfaclem3  19957  ocv1  21232  resttopon  22665  restabs  22669  restopnb  22679  restperf  22688  ordtbas  22696  ordtrest2lem  22707  ordtrest2  22708  leordtvallem1  22714  leordtvallem2  22715  cnclsi  22776  ordtt1  22883  cmpsub  22904  connsub  22925  cnconn  22926  nconnsubb  22927  connsubclo  22928  1stcfb  22949  kgentopon  23042  ptbasfi  23085  ptclsg  23119  dfac14lem  23121  xkoccn  23123  txcnmpt  23128  txtube  23144  xkoptsub  23158  xkopt  23159  kqsat  23235  kqcldsat  23237  ordthmeolem  23305  fbasrn  23388  trfil1  23390  trfil2  23391  trufil  23414  qustgphaus  23627  trust  23734  metustfbas  24066  cfilucfil  24068  xrsmopn  24328  lebnumii  24482  iscmet3  24810  resscdrg  24875  cmmbl  25051  voliunlem3  25069  uniioombllem4  25103  mbflimsup  25183  0plef  25189  0pledm  25190  itg1ge0  25203  mbfi1fseqlem5  25237  itg2addlem  25276  dvcmulf  25462  lhop1  25531  lhop2  25532  efopn  26166  wilthlem2  26573  ex-in  29709  cmcmlem  30875  pjvec  30980  pjocvec  30981  ssmd2  31596  mdslmd4i  31617  chirredlem2  31675  chirredlem3  31676  dmdbr7ati  31708  difuncomp  31816  xppreima  31902  suppovss  31937  fressupp  31941  gtiso  31953  preiman0  31962  fsuppcurry1  31981  fsuppcurry2  31982  resf1o  31986  elrspunidl  32577  ply1degltdimlem  32738  rspectopn  32878  prsss  32927  ordtrestNEW  32932  ordtrest2NEWlem  32933  ordtrest2NEW  32934  lmxrge0  32963  carsggect  33348  probdsb  33452  totprobd  33456  cndprobtot  33466  orvcelval  33498  ballotlemfmpn  33524  signsplypnf  33592  signsply0  33593  dfon2lem4  34789  neibastop3  35295  bj-restsnss  36012  bj-ismoored2  36037  bj-inexeqex  36083  bj-idreseq  36091  topdifinfeq  36279  poimirlem3  36539  poimirlem9  36545  mblfinlem3  36575  mblfinlem4  36576  itg2addnclem2  36588  blssp  36672  sstotbnd2  36690  lcvexchlem1  37952  lcvexchlem4  37955  glbconN  38295  glbconNOLD  38296  pmapglb2N  38690  pmapglb2xN  38691  2polssN  38834  polatN  38850  osumcllem1N  38875  osumcllem9N  38883  pexmidlem6N  38894  diarnN  40048  dihmeetlem11N  40236  dochexmidlem6  40384  lclkrlem2r  40443  mapdunirnN  40569  fsuppssindlem2  41212  prjcrv0  41423  ofoafg  42152  harval3  42337  rfovcnvf1od  42803  fsovcnvlem  42812  ntrneifv3  42881  ntrneifv4  42884  clsneifv3  42909  clsneifv4  42910  neicvgfv  42920  k0004lem2  42947  wnefimgd  42961  inabs3  43791  stoweidlem50  44814  sge0iunmptlemre  45179  caratheodorylem1  45290  smfconst  45513  fresfo  45806  funfocofob  45834  restclsseplem  47595