Theorem sseqin2 4203

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 3949	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2		incom 4189	. . 3 ⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴)
3	2	eqeq1i 2741	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 ↔ (𝐵 ∩ 𝐴) = 𝐴)
4	1, 3	bitri 275	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∩ 𝐴) = 𝐴)

Syntax hints:   ↔ wb 206   = wceq 1540   ∩ cin 3930   ⊆ wss 3931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-in 3938  df-ss 3948

This theorem is referenced by:  dfss4  4249  rintn0  5090  resabs1  5998  resima2  6008  xpssres  6010  mptimass  6065  rescnvcnv  6198  sspred  6304  trpred  6325  predres  6333  onfr  6396  ordtri2or3  6459  fndmdif  7037  fimacnvinrn2  7067  fveqressseq  7074  sorpssin  7730  cnvoprab  8064  frpoins3xpg  8144  frpoins3xp3g  8145  xpord3pred  8156  fsuppeq  8179  fsuppeqg  8180  frrlem4  8293  wfrlem4OLD  8331  fiint  9343  fiintOLD  9344  infxpenlem  10032  acndom2  10073  ackbij1lem2  10239  isf34lem5  10397  fpwwe2  10662  uzin  12897  iooval2  13400  fzval2  13532  leiso  14482  fz1isolem  14484  isercolllem3  15688  incexc  15858  bitsinv1  16466  bitsinvp1  16473  bitsshft  16499  dfphi2  16798  ressbas  17262  ressress  17273  ressabs  17274  psssdm  18597  sylow3lem2  19614  gsumxp  19962  dprdsn  20024  ablfac1eu  20061  pgpfac1lem5  20067  ablfaclem3  20075  ocv1  21644  resttopon  23104  restabs  23108  restopnb  23118  restperf  23127  ordtbas  23135  ordtrest2lem  23146  ordtrest2  23147  leordtvallem1  23153  leordtvallem2  23154  cnclsi  23215  ordtt1  23322  cmpsub  23343  connsub  23364  cnconn  23365  nconnsubb  23366  connsubclo  23367  1stcfb  23388  kgentopon  23481  ptbasfi  23524  ptclsg  23558  dfac14lem  23560  xkoccn  23562  txcnmpt  23567  txtube  23583  xkoptsub  23597  xkopt  23598  kqsat  23674  kqcldsat  23676  ordthmeolem  23744  fbasrn  23827  trfil1  23829  trfil2  23830  trufil  23853  qustgphaus  24066  trust  24173  metustfbas  24501  cfilucfil  24503  xrsmopn  24757  lebnumii  24921  iscmet3  25250  resscdrg  25315  cmmbl  25492  voliunlem3  25510  uniioombllem4  25544  mbflimsup  25624  0plef  25630  0pledm  25631  itg1ge0  25644  mbfi1fseqlem5  25677  itg2addlem  25716  dvcmulf  25905  lhop1  25976  lhop2  25977  efopn  26624  wilthlem2  27036  ex-in  30411  cmcmlem  31577  pjvec  31682  pjocvec  31683  ssmd2  32298  mdslmd4i  32319  chirredlem2  32377  chirredlem3  32378  dmdbr7ati  32410  difuncomp  32539  xppreima  32628  suppovss  32663  fressupp  32670  gtiso  32683  preiman0  32692  fsuppcurry1  32707  fsuppcurry2  32708  resf1o  32712  elrgspnsubrunlem2  33248  elrspunidl  33448  ply1degltdimlem  33667  fldgenfldext  33714  rspectopn  33903  prsss  33952  ordtrestNEW  33957  ordtrest2NEWlem  33958  ordtrest2NEW  33959  lmxrge0  33988  carsggect  34355  probdsb  34459  totprobd  34463  cndprobtot  34473  orvcelval  34506  ballotlemfmpn  34532  signsplypnf  34587  signsply0  34588  dfon2lem4  35809  neibastop3  36385  weiunfrlem  36487  bj-restsnss  37106  bj-ismoored2  37131  bj-inexeqex  37177  bj-idreseq  37185  topdifinfeq  37373  poimirlem3  37652  poimirlem9  37658  mblfinlem3  37688  mblfinlem4  37689  itg2addnclem2  37701  blssp  37785  sstotbnd2  37803  lcvexchlem1  39057  lcvexchlem4  39060  glbconN  39400  glbconNOLD  39401  pmapglb2N  39795  pmapglb2xN  39796  2polssN  39939  polatN  39955  osumcllem1N  39980  osumcllem9N  39988  pexmidlem6N  39999  diarnN  41153  dihmeetlem11N  41341  dochexmidlem6  41489  lclkrlem2r  41548  mapdunirnN  41674  fsuppssindlem2  42590  prjcrv0  42631  ofoafg  43353  harval3  43537  rfovcnvf1od  44003  fsovcnvlem  44012  ntrneifv3  44081  ntrneifv4  44084  clsneifv3  44109  clsneifv4  44110  neicvgfv  44120  k0004lem2  44147  wnefimgd  44160  inabs3  45060  stoweidlem50  46059  sge0iunmptlemre  46424  caratheodorylem1  46535  smfconst  46758  fresfo  47057  funfocofob  47087  grimuhgr  47880  restclsseplem  48869  incat  49458