Theorem sseqin2 4175

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

Syntax hints:   ↔ wb 206   = wceq 1541   ∩ cin 3900   ⊆ wss 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-in 3908  df-ss 3918

This theorem is referenced by:  dfss4  4221  rintn0  5064  resabs1  5965  resima2  5975  xpssres  5977  mptimass  6032  rescnvcnv  6162  sspred  6268  trpred  6289  predres  6297  onfr  6356  ordtri2or3  6419  fndmdif  6987  fimacnvinrn2  7017  fveqressseq  7024  sorpssin  7676  cnvoprab  8004  frpoins3xpg  8082  frpoins3xp3g  8083  xpord3pred  8094  fsuppeq  8117  fsuppeqg  8118  frrlem4  8231  fiint  9227  infxpenlem  9923  acndom2  9964  ackbij1lem2  10130  isf34lem5  10288  fpwwe2  10554  uzin  12787  iooval2  13294  fzval2  13426  leiso  14382  fz1isolem  14384  isercolllem3  15590  incexc  15760  bitsinv1  16369  bitsinvp1  16376  bitsshft  16402  dfphi2  16701  ressbas  17163  ressress  17174  ressabs  17175  psssdm  18505  sylow3lem2  19557  gsumxp  19905  dprdsn  19967  ablfac1eu  20004  pgpfac1lem5  20010  ablfaclem3  20018  ocv1  21634  resttopon  23105  restabs  23109  restopnb  23119  restperf  23128  ordtbas  23136  ordtrest2lem  23147  ordtrest2  23148  leordtvallem1  23154  leordtvallem2  23155  cnclsi  23216  ordtt1  23323  cmpsub  23344  connsub  23365  cnconn  23366  nconnsubb  23367  connsubclo  23368  1stcfb  23389  kgentopon  23482  ptbasfi  23525  ptclsg  23559  dfac14lem  23561  xkoccn  23563  txcnmpt  23568  txtube  23584  xkoptsub  23598  xkopt  23599  kqsat  23675  kqcldsat  23677  ordthmeolem  23745  fbasrn  23828  trfil1  23830  trfil2  23831  trufil  23854  qustgphaus  24067  trust  24173  metustfbas  24501  cfilucfil  24503  xrsmopn  24757  lebnumii  24921  iscmet3  25249  resscdrg  25314  cmmbl  25491  voliunlem3  25509  uniioombllem4  25543  mbflimsup  25623  0plef  25629  0pledm  25630  itg1ge0  25643  mbfi1fseqlem5  25676  itg2addlem  25715  dvcmulf  25904  lhop1  25975  lhop2  25976  efopn  26623  wilthlem2  27035  ex-in  30500  cmcmlem  31666  pjvec  31771  pjocvec  31772  ssmd2  32387  mdslmd4i  32408  chirredlem2  32466  chirredlem3  32467  dmdbr7ati  32499  difuncomp  32628  xppreima  32723  partfun2  32755  suppovss  32760  fressupp  32767  gtiso  32780  preiman0  32789  fsuppcurry1  32803  fsuppcurry2  32804  resf1o  32809  elrgspnsubrunlem2  33330  elrspunidl  33509  ply1degltdimlem  33779  fldgenfldext  33825  rspectopn  34024  prsss  34073  ordtrestNEW  34078  ordtrest2NEWlem  34079  ordtrest2NEW  34080  lmxrge0  34109  carsggect  34475  probdsb  34579  totprobd  34583  cndprobtot  34593  orvcelval  34626  ballotlemfmpn  34652  signsplypnf  34707  signsply0  34708  dfon2lem4  35978  neibastop3  36556  weiunfrlem  36658  bj-restsnss  37288  bj-ismoored2  37313  bj-inexeqex  37359  bj-idreseq  37367  topdifinfeq  37555  poimirlem3  37824  poimirlem9  37830  mblfinlem3  37860  mblfinlem4  37861  itg2addnclem2  37873  blssp  37957  sstotbnd2  37975  lcvexchlem1  39294  lcvexchlem4  39297  glbconN  39637  pmapglb2N  40031  pmapglb2xN  40032  2polssN  40175  polatN  40191  osumcllem1N  40216  osumcllem9N  40224  pexmidlem6N  40235  diarnN  41389  dihmeetlem11N  41577  dochexmidlem6  41725  lclkrlem2r  41784  mapdunirnN  41910  fsuppssindlem2  42835  prjcrv0  42876  ofoafg  43596  harval3  43779  rfovcnvf1od  44245  fsovcnvlem  44254  ntrneifv3  44323  ntrneifv4  44326  clsneifv3  44351  clsneifv4  44352  neicvgfv  44362  k0004lem2  44389  wnefimgd  44402  inabs3  45301  stoweidlem50  46294  sge0iunmptlemre  46659  caratheodorylem1  46770  smfconst  46993  fresfo  47294  funfocofob  47324  grimuhgr  48133  restclsseplem  49160  incat  49846