Theorem sseqin2 3817

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 3588	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2		incom 3805	. . 3 ⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴)
3	2	eqeq1i 2627	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 ↔ (𝐵 ∩ 𝐴) = 𝐴)
4	1, 3	bitri 264	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∩ 𝐴) = 𝐴)

Syntax hints:   ↔ wb 196   = wceq 1483   ∩ cin 3573   ⊆ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-ss 3588

This theorem is referenced by:  dfss5OLD  3819  sseqin2OLD  3832  dfss4  3858  rintn0  4619  resabs1  5427  resima2  5432  xpssres  5434  rescnvcnv  5597  sspred  5688  onfr  5763  ordtri2or3  5824  fndmdif  6321  fimacnvinrn2  6349  fveqressseq  6355  sorpssin  6945  predon  6991  omsinds  7084  frnsuppeq  7307  wfrlem4  7418  fiint  8237  infxpenlem  8836  acndom2  8877  ackbij1lem2  9043  isf34lem5  9200  fpwwe2  9465  uzin  11720  iooval2  12208  fzval2  12329  leiso  13243  fz1isolem  13245  isercolllem3  14397  incexc  14569  bitsinv1  15164  bitsinvp1  15171  bitsshft  15197  dfphi2  15479  ressbas  15930  ressress  15938  ressabs  15939  psssdm  17216  sylow3lem2  18043  gsumxp  18375  dprdsn  18435  ablfac1eu  18472  pgpfac1lem5  18478  ablfaclem3  18486  ocv1  20023  resttopon  20965  restabs  20969  restopnb  20979  restperf  20988  ordtbas  20996  ordtrest2lem  21007  ordtrest2  21008  leordtvallem1  21014  leordtvallem2  21015  cnclsi  21076  ordtt1  21183  cmpsub  21203  connsub  21224  cnconn  21225  nconnsubb  21226  connsubclo  21227  1stcfb  21248  kgentopon  21341  ptbasfi  21384  ptclsg  21418  dfac14lem  21420  xkoccn  21422  txcnmpt  21427  txtube  21443  xkoptsub  21457  xkopt  21458  kqsat  21534  kqcldsat  21536  ordthmeolem  21604  fbasrn  21688  trfil1  21690  trfil2  21691  trufil  21714  qustgphaus  21926  trust  22033  metustfbas  22362  cfilucfil  22364  xrsmopn  22615  lebnumii  22765  iscmet3  23091  resscdrg  23154  cmmbl  23302  voliunlem3  23320  uniioombllem4  23354  mbflimsup  23433  0plef  23439  0pledm  23440  itg1ge0  23453  mbfi1fseqlem5  23486  itg2addlem  23525  dvcmulf  23708  lhop1  23777  lhop2  23778  efopn  24404  wilthlem2  24795  ex-in  27282  cmcmlem  28450  pjvec  28555  pjocvec  28556  ssmd2  29171  mdslmd4i  29192  chirredlem2  29250  chirredlem3  29251  dmdbr7ati  29283  difuncomp  29369  xppreima  29449  gtiso  29478  resf1o  29505  prsss  29962  ordtrestNEW  29967  ordtrest2NEWlem  29968  ordtrest2NEW  29969  lmxrge0  29998  carsggect  30380  probdsb  30484  totprobd  30488  cndprobtot  30498  orvcelval  30530  ballotlemfmpn  30556  signsplypnf  30627  signsply0  30628  dfon2lem4  31691  frrlem4  31783  neibastop3  32357  bj-restsnss  33036  bj-ismoored2  33063  bj-ismooredr2  33065  topdifinfeq  33198  poimirlem3  33412  poimirlem9  33418  mblfinlem3  33448  mblfinlem4  33449  itg2addnclem2  33462  blssp  33552  sstotbnd2  33573  lcvexchlem1  34321  lcvexchlem4  34324  glbconN  34663  pmapglb2N  35057  pmapglb2xN  35058  2polssN  35201  polatN  35217  osumcllem1N  35242  osumcllem9N  35250  pexmidlem6N  35261  diarnN  36418  dihmeetlem11N  36606  dochexmidlem6  36754  lclkrlem2r  36813  mapdunirnN  36939  rfovcnvf1od  38298  fsovcnvlem  38307  ntrneifv3  38380  ntrneifv4  38383  clsneifv3  38408  clsneifv4  38409  neicvgfv  38419  k0004lem2  38446  wnefimgd  38460  inabs3  39224  mptima2  39457  stoweidlem50  40267  sge0iunmptlemre  40632  caratheodorylem1  40740  smfconst  40958