Theorem sseqin2 4107

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 3861	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2		incom 4092	. . 3 ⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴)
3	2	eqeq1i 2744	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 ↔ (𝐵 ∩ 𝐴) = 𝐴)
4	1, 3	bitri 278	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∩ 𝐴) = 𝐴)

Syntax hints:   ↔ wb 209   = wceq 1542   ∩ cin 3843   ⊆ wss 3844

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-9 2124  ax-ext 2711

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-rab 3063  df-in 3851  df-ss 3861

This theorem is referenced by:  dfss4  4150  rintn0  4995  resabs1  5856  resima2  5861  xpssres  5863  rescnvcnv  6037  sspred  6138  onfr  6212  ordtri2or3  6270  fndmdif  6822  fimacnvinrn2  6853  fveqressseq  6860  sorpssin  7478  predon  7528  omsinds  7622  cnvoprab  7786  frnsuppeq  7873  frnsuppeqg  7874  wfrlem4  7990  fiint  8872  infxpenlem  9516  acndom2  9557  ackbij1lem2  9724  isf34lem5  9881  fpwwe2  10146  uzin  12363  iooval2  12857  fzval2  12987  leiso  13914  fz1isolem  13916  isercolllem3  15119  incexc  15288  bitsinv1  15888  bitsinvp1  15895  bitsshft  15921  dfphi2  16214  ressbas  16660  ressress  16668  ressabs  16669  psssdm  17945  sylow3lem2  18874  gsumxp  19218  dprdsn  19280  ablfac1eu  19317  pgpfac1lem5  19323  ablfaclem3  19331  ocv1  20498  resttopon  21915  restabs  21919  restopnb  21929  restperf  21938  ordtbas  21946  ordtrest2lem  21957  ordtrest2  21958  leordtvallem1  21964  leordtvallem2  21965  cnclsi  22026  ordtt1  22133  cmpsub  22154  connsub  22175  cnconn  22176  nconnsubb  22177  connsubclo  22178  1stcfb  22199  kgentopon  22292  ptbasfi  22335  ptclsg  22369  dfac14lem  22371  xkoccn  22373  txcnmpt  22378  txtube  22394  xkoptsub  22408  xkopt  22409  kqsat  22485  kqcldsat  22487  ordthmeolem  22555  fbasrn  22638  trfil1  22640  trfil2  22641  trufil  22664  qustgphaus  22877  trust  22984  metustfbas  23313  cfilucfil  23315  xrsmopn  23567  lebnumii  23721  iscmet3  24048  resscdrg  24113  cmmbl  24289  voliunlem3  24307  uniioombllem4  24341  mbflimsup  24421  0plef  24427  0pledm  24428  itg1ge0  24441  mbfi1fseqlem5  24475  itg2addlem  24514  dvcmulf  24700  lhop1  24769  lhop2  24770  efopn  25404  wilthlem2  25809  ex-in  28365  cmcmlem  29529  pjvec  29634  pjocvec  29635  ssmd2  30250  mdslmd4i  30271  chirredlem2  30329  chirredlem3  30330  dmdbr7ati  30362  difuncomp  30470  xppreima  30560  suppovss  30595  fressupp  30600  gtiso  30611  preiman0  30620  fsuppcurry1  30638  fsuppcurry2  30639  resf1o  30643  elrspunidl  31181  rspectopn  31392  prsss  31441  ordtrestNEW  31446  ordtrest2NEWlem  31447  ordtrest2NEW  31448  lmxrge0  31477  carsggect  31858  probdsb  31962  totprobd  31966  cndprobtot  31976  orvcelval  32008  ballotlemfmpn  32034  signsplypnf  32102  signsply0  32103  dfon2lem4  33339  frpoins3xpg  33393  frpoins3xp3g  33394  xpord3pred  33414  frrlem4  33449  neibastop3  34197  bj-restsnss  34898  bj-ismoored2  34923  bj-inexeqex  34969  bj-idreseq  34977  topdifinfeq  35167  poimirlem3  35426  poimirlem9  35432  mblfinlem3  35462  mblfinlem4  35463  itg2addnclem2  35475  blssp  35560  sstotbnd2  35578  lcvexchlem1  36694  lcvexchlem4  36697  glbconN  37037  pmapglb2N  37431  pmapglb2xN  37432  2polssN  37575  polatN  37591  osumcllem1N  37616  osumcllem9N  37624  pexmidlem6N  37635  diarnN  38789  dihmeetlem11N  38977  dochexmidlem6  39125  lclkrlem2r  39184  mapdunirnN  39310  fsuppssindlem2  39883  harval3  40720  rfovcnvf1od  41181  fsovcnvlem  41190  ntrneifv3  41261  ntrneifv4  41264  clsneifv3  41289  clsneifv4  41290  neicvgfv  41300  k0004lem2  41327  wnefimgd  41341  inabs3  42165  mptima2  42351  stoweidlem50  43156  sge0iunmptlemre  43518  caratheodorylem1  43629  smfconst  43847  fresfo  44104  funfocofob  44132  restclsseplem  45760