Theorem sseqin2 4172

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ∩ cin 3901   ⊆ wss 3902

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-in 3909  df-ss 3919

This theorem is used by:  dfss4  4218  rintn0  5073  resabs1  6003  resima2  6013  xpssres  6015  mptimass  6073  rescnvcnv  6204  sspred  6312  trpred  6333  predres  6341  onfr  6401  ordtri2or3  6464  fndmdif  7038  fimacnvinrn2  7068  fveqressseq  7075  sorpssin  7735  cnvoprab  8060  frpoins3xpg  8141  frpoins3xp3g  8142  xpord3pred  8153  fsuppeq  8176  fsuppeqg  8177  frrlem4  8291  fiint  9299  infxpenlem  10019  acndom2  10060  ackbij1lem2  10225  isf34lem5  10383  fpwwe2  10655  uzin  12926  iooval2  13433  fzval2  13566  leiso  14526  fz1isolem  14528  isercolllem3  15756  incexc  15928  bitsinv1  16536  bitsinvp1  16543  bitsshft  16569  dfphi2  16869  ressbas  17332  ressress  17343  ressabs  17344  psssdm  18674  sylow3lem2  19759  gsumxp  20107  dprdsn  20169  ablfac1eu  20206  pgpfac1lem5  20212  ablfaclem3  20220  ocv1  21896  resttopon  23390  restabs  23394  restopnb  23404  restperf  23413  ordtbas  23421  ordtrest2lem  23432  ordtrest2  23433  leordtvallem1  23439  leordtvallem2  23440  cnclsi  23501  ordtt1  23608  cmpsub  23629  connsub  23650  cnconn  23651  nconnsubb  23652  connsubclo  23653  1stcfb  23674  kgentopon  23768  ptbasfi  23811  ptclsg  23845  dfac14lem  23847  xkoccn  23849  txcnmpt  23854  txtube  23870  xkoptsub  23884  xkopt  23885  kqsat  23961  kqcldsat  23963  ordthmeolem  24031  fbasrn  24114  trfil1  24116  trfil2  24117  trufil  24140  qustgphaus  24353  trust  24459  metustfbas  24787  cfilucfil  24789  xrsmopn  25043  lebnumii  25198  iscmet3  25525  resscdrg  25590  cmmbl  25766  voliunlem3  25784  uniioombllem4  25818  mbflimsup  25898  0plef  25904  0pledm  25905  itg1ge0  25918  mbfi1fseqlem5  25951  itg2addlem  25990  dvcmulf  26177  lhop1  26246  lhop2  26247  efopn  26896  wilthlem2  27306  ex-in  30906  cmcmlem  32073  pjvec  32178  pjocvec  32179  ssmd2  32794  mdslmd4i  32815  chirredlem2  32873  chirredlem3  32874  dmdbr7ati  32906  difuncomp  33028  xppreima  33120  partfun2  33151  suppovss  33155  fressupp  33162  gtiso  33175  preiman0  33184  fsuppcurry1  33197  fsuppcurry2  33198  resf1o  33203  elrgspnsubrunlem2  33690  elrspunidl  33858  ply1degltdimlem  34134  fldgenfldext  34180  rspectopn  34379  prsss  34428  ordtrestNEW  34433  ordtrest2NEWlem  34434  ordtrest2NEW  34435  lmxrge0  34464  carsggect  34831  probdsb  34935  totprobd  34939  cndprobtot  34949  orvcelval  34982  ballotlemfmpn  35008  signsplypnf  35060  signsply0  35061  dfon2lem4  36365  neibastop3  36983  weiunfrlem  37085  bj-restsnss  37835  bj-ismoored2  37860  bj-inexeqex  37908  bj-idreseq  37916  topdifinfeq  38106  poimirlem3  38374  poimirlem9  38380  mblfinlem3  38410  mblfinlem4  38411  itg2addnclem2  38423  blssp  38508  sstotbnd2  38526  lcvexchlem1  39909  lcvexchlem4  39912  glbconN  40252  pmapglb2N  40646  pmapglb2xN  40647  2polssN  40790  polatN  40806  osumcllem1N  40831  osumcllem9N  40839  pexmidlem6N  40850  diarnN  42004  dihmeetlem11N  42192  dochexmidlem6  42340  lclkrlem2r  42399  mapdunirnN  42525  fsuppssindlem2  43440  prjcrv0  43481  ofoafg  44197  harval3  44380  rfovcnvf1od  44846  fsovcnvlem  44855  ntrneifv3  44924  ntrneifv4  44927  clsneifv3  44952  clsneifv4  44953  neicvgfv  44963  k0004lem2  44990  wnefimgd  45003  inabs3  45892  stoweidlem50  46880  sge0iunmptlemre  47245  caratheodorylem1  47356  smfconst  47579  fresfo  47938  funfocofob  47968  grimuhgr  48805  restclsseplem  49843  incat  50529