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

Syntax hints:   ↔ wb 209   = wceq 1568   ∩ cin 3903   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-tru 1571  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3415  df-in 3911  df-ss 3921

This theorem is referenced by:  dfss4  4221  rintn0  5074  resabs1  6005  resima2  6015  xpssres  6017  mptimass  6075  rescnvcnv  6205  sspred  6311  trpred  6332  predres  6340  onfr  6400  ordtri2or3  6463  fndmdif  7037  fimacnvinrn2  7067  fveqressseq  7074  sorpssin  7728  cnvoprab  8056  frpoins3xpg  8135  frpoins3xp3g  8136  xpord3pred  8147  fsuppeq  8170  fsuppeqg  8171  frrlem4  8285  fiint  9285  infxpenlem  9996  acndom2  10037  ackbij1lem2  10202  isf34lem5  10361  fpwwe2  10627  uzin  12897  iooval2  13404  fzval2  13537  leiso  14496  fz1isolem  14498  isercolllem3  15718  incexc  15891  bitsinv1  16499  bitsinvp1  16506  bitsshft  16532  dfphi2  16832  ressbas  17295  ressress  17306  ressabs  17307  psssdm  18637  sylow3lem2  19697  gsumxp  20045  dprdsn  20107  ablfac1eu  20144  pgpfac1lem5  20150  ablfaclem3  20158  ocv1  21808  resttopon  23297  restabs  23301  restopnb  23311  restperf  23320  ordtbas  23328  ordtrest2lem  23339  ordtrest2  23340  leordtvallem1  23346  leordtvallem2  23347  cnclsi  23408  ordtt1  23515  cmpsub  23536  connsub  23557  cnconn  23558  nconnsubb  23559  connsubclo  23560  1stcfb  23581  kgentopon  23674  ptbasfi  23717  ptclsg  23751  dfac14lem  23753  xkoccn  23755  txcnmpt  23760  txtube  23776  xkoptsub  23790  xkopt  23791  kqsat  23867  kqcldsat  23869  ordthmeolem  23937  fbasrn  24020  trfil1  24022  trfil2  24023  trufil  24046  qustgphaus  24259  trust  24365  metustfbas  24693  cfilucfil  24695  xrsmopn  24949  lebnumii  25104  iscmet3  25431  resscdrg  25496  cmmbl  25672  voliunlem3  25690  uniioombllem4  25724  mbflimsup  25804  0plef  25810  0pledm  25811  itg1ge0  25824  mbfi1fseqlem5  25857  itg2addlem  25896  dvcmulf  26083  lhop1  26152  lhop2  26153  efopn  26799  wilthlem2  27209  ex-in  30742  cmcmlem  31909  pjvec  32014  pjocvec  32015  ssmd2  32630  mdslmd4i  32651  chirredlem2  32709  chirredlem3  32710  dmdbr7ati  32742  difuncomp  32864  xppreima  32956  partfun2  32987  suppovss  32992  fressupp  32999  gtiso  33012  preiman0  33021  fsuppcurry1  33035  fsuppcurry2  33036  resf1o  33041  elrgspnsubrunlem2  33534  elrspunidl  33702  ply1degltdimlem  33978  fldgenfldext  34024  rspectopn  34223  prsss  34272  ordtrestNEW  34277  ordtrest2NEWlem  34278  ordtrest2NEW  34279  lmxrge0  34308  carsggect  34674  probdsb  34778  totprobd  34782  cndprobtot  34792  orvcelval  34825  ballotlemfmpn  34851  signsplypnf  34903  signsply0  34904  dfon2lem4  36242  neibastop3  36839  weiunfrlem  36941  bj-restsnss  37691  bj-ismoored2  37716  bj-inexeqex  37764  bj-idreseq  37772  topdifinfeq  37962  poimirlem3  38240  poimirlem9  38246  mblfinlem3  38276  mblfinlem4  38277  itg2addnclem2  38289  blssp  38373  sstotbnd2  38391  lcvexchlem1  39776  lcvexchlem4  39779  glbconN  40119  pmapglb2N  40513  pmapglb2xN  40514  2polssN  40657  polatN  40673  osumcllem1N  40698  osumcllem9N  40706  pexmidlem6N  40717  diarnN  41871  dihmeetlem11N  42059  dochexmidlem6  42207  lclkrlem2r  42266  mapdunirnN  42392  fsuppssindlem2  43294  prjcrv0  43335  ofoafg  44051  harval3  44234  rfovcnvf1od  44700  fsovcnvlem  44709  ntrneifv3  44778  ntrneifv4  44781  clsneifv3  44806  clsneifv4  44807  neicvgfv  44817  k0004lem2  44844  wnefimgd  44857  inabs3  45746  stoweidlem50  46734  sge0iunmptlemre  47099  caratheodorylem1  47210  smfconst  47433  fresfo  47752  funfocofob  47782  grimuhgr  48619  restclsseplem  49660  incat  50346