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 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∩ 𝐴) = 𝐴)

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-3an 1104  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416  df-in 3911  df-ss 3921

This theorem is used by:  dfss4  4221  rintn0  5074  resabs1  6004  resima2  6014  xpssres  6016  mptimass  6074  rescnvcnv  6204  sspred  6311  trpred  6332  predres  6340  onfr  6400  ordtri2or3  6463  fndmdif  7037  fimacnvinrn2  7067  fveqressseq  7074  sorpssin  7730  cnvoprab  8055  frpoins3xpg  8134  frpoins3xp3g  8135  xpord3pred  8146  fsuppeq  8169  fsuppeqg  8170  frrlem4  8284  fiint  9284  infxpenlem  10004  acndom2  10045  ackbij1lem2  10210  isf34lem5  10368  fpwwe2  10634  uzin  12904  iooval2  13411  fzval2  13544  leiso  14503  fz1isolem  14505  isercolllem3  15725  incexc  15898  bitsinv1  16506  bitsinvp1  16513  bitsshft  16539  dfphi2  16839  ressbas  17302  ressress  17313  ressabs  17314  psssdm  18644  sylow3lem2  19704  gsumxp  20052  dprdsn  20114  ablfac1eu  20151  pgpfac1lem5  20157  ablfaclem3  20165  ocv1  21840  resttopon  23329  restabs  23333  restopnb  23343  restperf  23352  ordtbas  23360  ordtrest2lem  23371  ordtrest2  23372  leordtvallem1  23378  leordtvallem2  23379  cnclsi  23440  ordtt1  23547  cmpsub  23568  connsub  23589  cnconn  23590  nconnsubb  23591  connsubclo  23592  1stcfb  23613  kgentopon  23706  ptbasfi  23749  ptclsg  23783  dfac14lem  23785  xkoccn  23787  txcnmpt  23792  txtube  23808  xkoptsub  23822  xkopt  23823  kqsat  23899  kqcldsat  23901  ordthmeolem  23969  fbasrn  24052  trfil1  24054  trfil2  24055  trufil  24078  qustgphaus  24291  trust  24397  metustfbas  24725  cfilucfil  24727  xrsmopn  24981  lebnumii  25136  iscmet3  25463  resscdrg  25528  cmmbl  25704  voliunlem3  25722  uniioombllem4  25756  mbflimsup  25836  0plef  25842  0pledm  25843  itg1ge0  25856  mbfi1fseqlem5  25889  itg2addlem  25928  dvcmulf  26115  lhop1  26184  lhop2  26185  efopn  26834  wilthlem2  27244  ex-in  30787  cmcmlem  31954  pjvec  32059  pjocvec  32060  ssmd2  32675  mdslmd4i  32696  chirredlem2  32754  chirredlem3  32755  dmdbr7ati  32787  difuncomp  32909  xppreima  33001  partfun2  33032  suppovss  33037  fressupp  33044  gtiso  33057  preiman0  33066  fsuppcurry1  33080  fsuppcurry2  33081  resf1o  33086  elrgspnsubrunlem2  33577  elrspunidl  33745  ply1degltdimlem  34021  fldgenfldext  34067  rspectopn  34266  prsss  34315  ordtrestNEW  34320  ordtrest2NEWlem  34321  ordtrest2NEW  34322  lmxrge0  34351  carsggect  34717  probdsb  34821  totprobd  34825  cndprobtot  34835  orvcelval  34868  ballotlemfmpn  34894  signsplypnf  34946  signsply0  34947  dfon2lem4  36284  neibastop3  36901  weiunfrlem  37003  bj-restsnss  37753  bj-ismoored2  37778  bj-inexeqex  37826  bj-idreseq  37834  topdifinfeq  38024  poimirlem3  38302  poimirlem9  38308  mblfinlem3  38338  mblfinlem4  38339  itg2addnclem2  38351  blssp  38435  sstotbnd2  38453  lcvexchlem1  39836  lcvexchlem4  39839  glbconN  40179  pmapglb2N  40573  pmapglb2xN  40574  2polssN  40717  polatN  40733  osumcllem1N  40758  osumcllem9N  40766  pexmidlem6N  40777  diarnN  41931  dihmeetlem11N  42119  dochexmidlem6  42267  lclkrlem2r  42326  mapdunirnN  42452  fsuppssindlem2  43352  prjcrv0  43393  ofoafg  44109  harval3  44292  rfovcnvf1od  44758  fsovcnvlem  44767  ntrneifv3  44836  ntrneifv4  44839  clsneifv3  44864  clsneifv4  44865  neicvgfv  44875  k0004lem2  44902  wnefimgd  44915  inabs3  45804  stoweidlem50  46792  sge0iunmptlemre  47157  caratheodorylem1  47268  smfconst  47491  fresfo  47813  funfocofob  47843  grimuhgr  48680  restclsseplem  49721  incat  50407