Theorem sseqin2 4168

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

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

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 2732

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-in 3905  df-ss 3915

This theorem is used by:  dfss4  4214  rintn0  5068  resabs1  5993  resima2  6003  xpssres  6005  mptimass  6063  rescnvcnv  6194  sspred  6302  trpred  6323  predres  6331  onfr  6391  ordtri2or3  6454  fndmdif  7029  fimacnvinrn2  7060  fveqressseq  7067  sorpssin  7730  cnvoprab  8054  frpoins3xpg  8135  frpoins3xp3g  8136  xpord3pred  8147  fsuppeq  8170  fsuppeqg  8171  frrlem4  8285  fiint  9296  infxpenlem  10064  acndom2  10105  ackbij1lem2  10270  isf34lem5  10428  fpwwe2  10700  uzin  12971  iooval2  13479  fzval2  13612  leiso  14572  fz1isolem  14574  isercolllem3  15802  incexc  15974  bitsinv1  16580  bitsinvp1  16587  bitsshft  16613  dfphi2  16913  ressbas  17376  ressress  17387  ressabs  17388  psssdm  18718  sylow3lem2  19804  gsumxp  20152  dprdsn  20214  ablfac1eu  20251  pgpfac1lem5  20257  ablfaclem3  20265  ocv1  21947  resttopon  23441  restabs  23445  restopnb  23455  restperf  23464  ordtbas  23472  ordtrest2lem  23483  ordtrest2  23484  leordtvallem1  23490  leordtvallem2  23491  cnclsi  23552  ordtt1  23659  cmpsub  23680  connsub  23701  cnconn  23702  nconnsubb  23703  connsubclo  23704  1stcfb  23725  kgentopon  23819  ptbasfi  23862  ptclsg  23896  dfac14lem  23898  xkoccn  23900  txcnmpt  23905  txtube  23921  xkoptsub  23935  xkopt  23936  kqsat  24012  kqcldsat  24014  ordthmeolem  24082  fbasrn  24165  trfil1  24167  trfil2  24168  trufil  24191  qustgphaus  24404  trust  24510  metustfbas  24838  cfilucfil  24840  xrsmopn  25094  lebnumii  25249  iscmet3  25576  resscdrg  25641  cmmbl  25817  voliunlem3  25835  uniioombllem4  25869  mbflimsup  25949  0plef  25955  0pledm  25956  itg1ge0  25969  mbfi1fseqlem5  26002  itg2addlem  26041  dvcmulf  26227  lhop1  26296  lhop2  26297  efopn  26950  wilthlem2  27360  ex-in  30960  cmcmlem  32127  pjvec  32232  pjocvec  32233  ssmd2  32848  mdslmd4i  32869  chirredlem2  32927  chirredlem3  32928  dmdbr7ati  32960  difuncomp  33082  xppreima  33173  partfun2  33204  suppovss  33208  fressupp  33215  gtiso  33228  preiman0  33237  fsuppcurry1  33250  fsuppcurry2  33251  resf1o  33256  elrgspnsubrunlem2  33743  elrspunidl  33912  ply1degltdimlem  34188  fldgenfldext  34234  rspectopn  34433  prsss  34482  ordtrestNEW  34487  ordtrest2NEWlem  34488  ordtrest2NEW  34489  lmxrge0  34518  carsggect  34885  probdsb  34989  totprobd  34993  cndprobtot  35003  orvcelval  35036  ballotlemfmpn  35062  signsplypnf  35114  signsply0  35115  dfon2lem4  36470  neibastop3  37072  weiunfrlem  37174  bj-restsnss  37924  bj-ismoored2  37949  bj-inexeqex  37995  bj-idreseq  38003  topdifinfeq  38193  poimirlem3  38461  poimirlem9  38467  mblfinlem3  38497  mblfinlem4  38498  itg2addnclem2  38510  blssp  38610  sstotbnd2  38628  lcvexchlem1  40011  lcvexchlem4  40014  glbconN  40354  pmapglb2N  40748  pmapglb2xN  40749  2polssN  40892  polatN  40908  osumcllem1N  40933  osumcllem9N  40941  pexmidlem6N  40952  diarnN  42106  dihmeetlem11N  42294  dochexmidlem6  42442  lclkrlem2r  42501  mapdunirnN  42627  fsuppssindlem2  43542  prjcrv0  43583  ofoafg  44299  harval3  44482  rfovcnvf1od  44948  fsovcnvlem  44957  ntrneifv3  45026  ntrneifv4  45029  clsneifv3  45054  clsneifv4  45055  neicvgfv  45065  k0004lem2  45092  wnefimgd  45105  inabs3  45994  stoweidlem50  46982  sge0iunmptlemre  47347  caratheodorylem1  47458  smfconst  47681  fresfo  48040  funfocofob  48070  grimuhgr  48907  restclsseplem  49945  incat  50631