Theorem sseqin2 4142

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

Syntax hints:   ↔ wb 209   = wceq 1538   ∩ cin 3880   ⊆ wss 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-rab 3115  df-in 3888  df-ss 3898

This theorem is referenced by:  dfss4  4185  rintn0  4994  resabs1  5848  resima2  5853  xpssres  5855  rescnvcnv  6028  sspred  6124  onfr  6198  ordtri2or3  6256  fndmdif  6789  fimacnvinrn2  6818  fveqressseq  6824  sorpssin  7437  predon  7486  omsinds  7580  cnvoprab  7740  frnsuppeq  7825  wfrlem4  7941  fiint  8779  infxpenlem  9424  acndom2  9465  ackbij1lem2  9632  isf34lem5  9789  fpwwe2  10054  uzin  12266  iooval2  12759  fzval2  12888  leiso  13813  fz1isolem  13815  isercolllem3  15015  incexc  15184  bitsinv1  15781  bitsinvp1  15788  bitsshft  15814  dfphi2  16101  ressbas  16546  ressress  16554  ressabs  16555  psssdm  17818  sylow3lem2  18745  gsumxp  19089  dprdsn  19151  ablfac1eu  19188  pgpfac1lem5  19194  ablfaclem3  19202  ocv1  20368  resttopon  21766  restabs  21770  restopnb  21780  restperf  21789  ordtbas  21797  ordtrest2lem  21808  ordtrest2  21809  leordtvallem1  21815  leordtvallem2  21816  cnclsi  21877  ordtt1  21984  cmpsub  22005  connsub  22026  cnconn  22027  nconnsubb  22028  connsubclo  22029  1stcfb  22050  kgentopon  22143  ptbasfi  22186  ptclsg  22220  dfac14lem  22222  xkoccn  22224  txcnmpt  22229  txtube  22245  xkoptsub  22259  xkopt  22260  kqsat  22336  kqcldsat  22338  ordthmeolem  22406  fbasrn  22489  trfil1  22491  trfil2  22492  trufil  22515  qustgphaus  22728  trust  22835  metustfbas  23164  cfilucfil  23166  xrsmopn  23417  lebnumii  23571  iscmet3  23897  resscdrg  23962  cmmbl  24138  voliunlem3  24156  uniioombllem4  24190  mbflimsup  24270  0plef  24276  0pledm  24277  itg1ge0  24290  mbfi1fseqlem5  24323  itg2addlem  24362  dvcmulf  24548  lhop1  24617  lhop2  24618  efopn  25249  wilthlem2  25654  ex-in  28210  cmcmlem  29374  pjvec  29479  pjocvec  29480  ssmd2  30095  mdslmd4i  30116  chirredlem2  30174  chirredlem3  30175  dmdbr7ati  30207  difuncomp  30317  xppreima  30408  suppovss  30443  fressupp  30448  gtiso  30460  preiman0  30469  fsuppcurry1  30487  fsuppcurry2  30488  resf1o  30492  elrspunidl  31014  rspectopn  31220  prsss  31269  ordtrestNEW  31274  ordtrest2NEWlem  31275  ordtrest2NEW  31276  lmxrge0  31305  carsggect  31686  probdsb  31790  totprobd  31794  cndprobtot  31804  orvcelval  31836  ballotlemfmpn  31862  signsplypnf  31930  signsply0  31931  dfon2lem4  33144  frrlem4  33239  neibastop3  33823  bj-restsnss  34498  bj-ismoored2  34523  bj-inexeqex  34569  bj-idreseq  34577  topdifinfeq  34767  poimirlem3  35060  poimirlem9  35066  mblfinlem3  35096  mblfinlem4  35097  itg2addnclem2  35109  blssp  35194  sstotbnd2  35212  lcvexchlem1  36330  lcvexchlem4  36333  glbconN  36673  pmapglb2N  37067  pmapglb2xN  37068  2polssN  37211  polatN  37227  osumcllem1N  37252  osumcllem9N  37260  pexmidlem6N  37271  diarnN  38425  dihmeetlem11N  38613  dochexmidlem6  38761  lclkrlem2r  38820  mapdunirnN  38946  fsuppssindlem2  39458  harval3  40244  rfovcnvf1od  40705  fsovcnvlem  40714  ntrneifv3  40785  ntrneifv4  40788  clsneifv3  40813  clsneifv4  40814  neicvgfv  40824  k0004lem2  40851  wnefimgd  40865  inabs3  41690  mptima2  41883  stoweidlem50  42692  sge0iunmptlemre  43054  caratheodorylem1  43165  smfconst  43383