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  j0ltalephlem  35939  dfon2lem4  36623  neibastop3  37225  weiunfrlem  37327  bj-restsnss  38079  bj-ismoored2  38104  bj-inexeqex  38151  bj-idreseq  38159  topdifinfeq  38349  poimirlem3  38617  poimirlem9  38623  mblfinlem3  38653  mblfinlem4  38654  itg2addnclem2  38666  blssp  38766  sstotbnd2  38784  lcvexchlem1  40167  lcvexchlem4  40170  glbconN  40510  pmapglb2N  40904  pmapglb2xN  40905  2polssN  41048  polatN  41064  osumcllem1N  41089  osumcllem9N  41097  pexmidlem6N  41108  diarnN  42262  dihmeetlem11N  42450  dochexmidlem6  42598  lclkrlem2r  42657  mapdunirnN  42783  fsuppssindlem2  43696  prjcrv0  43745  ofoafg  44432  harval3  44615  rfovcnvf1od  45080  fsovcnvlem  45089  ntrneifv3  45158  ntrneifv4  45161  clsneifv3  45186  clsneifv4  45187  neicvgfv  45197  k0004lem2  45224  wnefimgd  45237  inabs3  46149  stoweidlem50  47136  sge0iunmptlemre  47501  caratheodorylem1  47612  smfconst  47835  fresfo  48194  funfocofob  48224  grimuhgr  49061  restclsseplem  50099  incat  50785