Theorem sseqin2 4223

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∩ cin 3950   ⊆ wss 3951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-in 3958  df-ss 3968

This theorem is referenced by:  dfss4  4269  rintn0  5109  resabs1  6024  resima2  6034  xpssres  6036  mptimass  6091  rescnvcnv  6224  sspred  6330  trpred  6352  predres  6360  onfr  6423  ordtri2or3  6484  fndmdif  7062  fimacnvinrn2  7092  fveqressseq  7099  sorpssin  7751  cnvoprab  8085  frpoins3xpg  8165  frpoins3xp3g  8166  xpord3pred  8177  fsuppeq  8200  fsuppeqg  8201  frrlem4  8314  wfrlem4OLD  8352  fiint  9366  fiintOLD  9367  infxpenlem  10053  acndom2  10094  ackbij1lem2  10260  isf34lem5  10418  fpwwe2  10683  uzin  12918  iooval2  13420  fzval2  13550  leiso  14498  fz1isolem  14500  isercolllem3  15703  incexc  15873  bitsinv1  16479  bitsinvp1  16486  bitsshft  16512  dfphi2  16811  ressbas  17280  ressbasOLD  17281  ressress  17293  ressabs  17294  psssdm  18627  sylow3lem2  19646  gsumxp  19994  dprdsn  20056  ablfac1eu  20093  pgpfac1lem5  20099  ablfaclem3  20107  ocv1  21697  resttopon  23169  restabs  23173  restopnb  23183  restperf  23192  ordtbas  23200  ordtrest2lem  23211  ordtrest2  23212  leordtvallem1  23218  leordtvallem2  23219  cnclsi  23280  ordtt1  23387  cmpsub  23408  connsub  23429  cnconn  23430  nconnsubb  23431  connsubclo  23432  1stcfb  23453  kgentopon  23546  ptbasfi  23589  ptclsg  23623  dfac14lem  23625  xkoccn  23627  txcnmpt  23632  txtube  23648  xkoptsub  23662  xkopt  23663  kqsat  23739  kqcldsat  23741  ordthmeolem  23809  fbasrn  23892  trfil1  23894  trfil2  23895  trufil  23918  qustgphaus  24131  trust  24238  metustfbas  24570  cfilucfil  24572  xrsmopn  24834  lebnumii  24998  iscmet3  25327  resscdrg  25392  cmmbl  25569  voliunlem3  25587  uniioombllem4  25621  mbflimsup  25701  0plef  25707  0pledm  25708  itg1ge0  25721  mbfi1fseqlem5  25754  itg2addlem  25793  dvcmulf  25982  lhop1  26053  lhop2  26054  efopn  26700  wilthlem2  27112  ex-in  30444  cmcmlem  31610  pjvec  31715  pjocvec  31716  ssmd2  32331  mdslmd4i  32352  chirredlem2  32410  chirredlem3  32411  dmdbr7ati  32443  difuncomp  32566  xppreima  32655  suppovss  32690  fressupp  32697  gtiso  32710  preiman0  32719  fsuppcurry1  32736  fsuppcurry2  32737  resf1o  32741  elrgspnsubrunlem2  33252  elrspunidl  33456  ply1degltdimlem  33673  fldgenfldext  33718  rspectopn  33866  prsss  33915  ordtrestNEW  33920  ordtrest2NEWlem  33921  ordtrest2NEW  33922  lmxrge0  33951  carsggect  34320  probdsb  34424  totprobd  34428  cndprobtot  34438  orvcelval  34471  ballotlemfmpn  34497  signsplypnf  34565  signsply0  34566  dfon2lem4  35787  neibastop3  36363  weiunfrlem  36465  bj-restsnss  37084  bj-ismoored2  37109  bj-inexeqex  37155  bj-idreseq  37163  topdifinfeq  37351  poimirlem3  37630  poimirlem9  37636  mblfinlem3  37666  mblfinlem4  37667  itg2addnclem2  37679  blssp  37763  sstotbnd2  37781  lcvexchlem1  39035  lcvexchlem4  39038  glbconN  39378  glbconNOLD  39379  pmapglb2N  39773  pmapglb2xN  39774  2polssN  39917  polatN  39933  osumcllem1N  39958  osumcllem9N  39966  pexmidlem6N  39977  diarnN  41131  dihmeetlem11N  41319  dochexmidlem6  41467  lclkrlem2r  41526  mapdunirnN  41652  fsuppssindlem2  42602  prjcrv0  42643  ofoafg  43367  harval3  43551  rfovcnvf1od  44017  fsovcnvlem  44026  ntrneifv3  44095  ntrneifv4  44098  clsneifv3  44123  clsneifv4  44124  neicvgfv  44134  k0004lem2  44161  wnefimgd  44174  inabs3  45061  stoweidlem50  46065  sge0iunmptlemre  46430  caratheodorylem1  46541  smfconst  46764  fresfo  47060  funfocofob  47090  grimuhgr  47878  restclsseplem  48812