Theorem sseqin2 4120

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1569   ⊆ wss 3895   ∩ cin 4089

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-ss 3896  df-in 4091

This theorem is used by:  dfss4  4214  rintn0  5068  resabs1  5996  xpssres  6006  resima2  6056  mptimass  6070  rescnvcnv  6205  sspred  6313  trpred  6334  predres  6342  onfr  6402  ordtri2or3  6465  fndmdif  7041  fimacnvinrn2  7072  fveqressseq  7079  sorpssin  7747  cnvoprab  8071  frpoins3xpg  8157  frpoins3xp3g  8158  xpord3pred  8169  fsuppeq  8193  fsuppeqg  8194  frrlem4  8308  fiint  9319  infxpenlem  10093  acndom2  10134  ackbij1lem2  10299  isf34lem5  10457  fpwwe2  10729  uzin  13002  iooval2  13510  fzval2  13643  leiso  14605  fz1isolem  14607  isercolllem3  15835  incexc  16007  bitsinv1  16613  bitsinvp1  16620  bitsshft  16646  dfphi2  16952  ressbas  17415  ressress  17426  ressabs  17427  psssdm  18757  sylow3lem2  19843  gsumxp  20191  dprdsn  20253  ablfac1eu  20290  pgpfac1lem5  20296  ablfaclem3  20304  ocv1  21986  resttopon  23480  restabs  23484  restopnb  23494  restperf  23503  ordtbas  23511  ordtrest2lem  23522  ordtrest2  23523  leordtvallem1  23529  leordtvallem2  23530  cnclsi  23591  ordtt1  23698  cmpsub  23719  connsub  23740  cnconn  23741  nconnsubb  23742  connsubclo  23743  1stcfb  23764  kgentopon  23858  ptbasfi  23901  ptclsg  23935  dfac14lem  23937  xkoccn  23939  txcnmpt  23944  txtube  23960  xkoptsub  23974  xkopt  23975  kqsat  24051  kqcldsat  24053  ordthmeolem  24121  fbasrn  24204  trfil1  24206  trfil2  24207  trufil  24230  qustgphaus  24443  trust  24549  metustfbas  24877  cfilucfil  24879  xrsmopn  25133  lebnumii  25288  iscmet3  25615  resscdrg  25680  cmmbl  25856  voliunlem3  25874  uniioombllem4  25908  mbflimsup  25988  0plef  25994  0pledm  25995  itg1ge0  26008  mbfi1fseqlem5  26041  itg2addlem  26080  dvcmulf  26266  lhop1  26335  lhop2  26336  efopn  26987  wilthlem2  27397  ex-in  31027  cmcmlem  32194  pjvec  32299  pjocvec  32300  ssmd2  32915  mdslmd4i  32936  chirredlem2  32994  chirredlem3  32995  dmdbr7ati  33027  difuncomp  33191  xppreima  33282  partfun2  33313  suppovss  33317  fressupp  33324  gtiso  33337  preiman0  33346  fsuppcurry1  33359  fsuppcurry2  33360  resf1o  33365  elrgspnsubrunlem2  33852  elrspunidl  34021  ply1degltdimlem  34297  fldgenfldext  34343  rspectopn  34542  prsss  34591  ordtrestNEW  34596  ordtrest2NEWlem  34597  ordtrest2NEW  34598  lmxrge0  34627  carsggect  34993  probdsb  35097  totprobd  35101  cndprobtot  35111  orvcelval  35144  ballotlemfmpn  35170  signsplypnf  35222  signsply0  35223  dfon2lem4  36591  neibastop3  37193  weiunfrlem  37295  bj-restsnss  38047  bj-ismoored2  38072  bj-inexeqex  38119  bj-idreseq  38127  topdifinfeq  38317  poimirlem3  38585  poimirlem9  38591  mblfinlem3  38621  mblfinlem4  38622  itg2addnclem2  38634  blssp  38734  sstotbnd2  38752  lcvexchlem1  40135  lcvexchlem4  40138  glbconN  40478  pmapglb2N  40872  pmapglb2xN  40873  2polssN  41016  polatN  41032  osumcllem1N  41057  osumcllem9N  41065  pexmidlem6N  41076  diarnN  42230  dihmeetlem11N  42418  dochexmidlem6  42566  lclkrlem2r  42625  mapdunirnN  42751  fsuppssindlem2  43664  prjcrv0  43713  ofoafg  44400  harval3  44583  rfovcnvf1od  45048  fsovcnvlem  45057  ntrneifv3  45126  ntrneifv4  45129  clsneifv3  45154  clsneifv4  45155  neicvgfv  45165  k0004lem2  45192  wnefimgd  45205  inabs3  46117  stoweidlem50  47104  sge0iunmptlemre  47469  caratheodorylem1  47580  smfconst  47803  fresfo  48162  funfocofob  48192  grimuhgr  49029  restclsseplem  50067  incat  50753