Theorem sseqin2 4174

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

Syntax hints:   ↔ wb 206   = wceq 1541   ∩ cin 3898   ⊆ wss 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3398  df-in 3906  df-ss 3916

This theorem is referenced by:  dfss4  4220  rintn0  5061  resabs1  5962  resima2  5972  xpssres  5974  mptimass  6029  rescnvcnv  6159  sspred  6265  trpred  6286  predres  6294  onfr  6353  ordtri2or3  6416  fndmdif  6984  fimacnvinrn2  7014  fveqressseq  7021  sorpssin  7673  cnvoprab  8001  frpoins3xpg  8079  frpoins3xp3g  8080  xpord3pred  8091  fsuppeq  8114  fsuppeqg  8115  frrlem4  8228  fiint  9221  infxpenlem  9914  acndom2  9955  ackbij1lem2  10121  isf34lem5  10279  fpwwe2  10544  uzin  12782  iooval2  13288  fzval2  13420  leiso  14376  fz1isolem  14378  isercolllem3  15584  incexc  15754  bitsinv1  16363  bitsinvp1  16370  bitsshft  16396  dfphi2  16695  ressbas  17157  ressress  17168  ressabs  17169  psssdm  18498  sylow3lem2  19550  gsumxp  19898  dprdsn  19960  ablfac1eu  19997  pgpfac1lem5  20003  ablfaclem3  20011  ocv1  21626  resttopon  23086  restabs  23090  restopnb  23100  restperf  23109  ordtbas  23117  ordtrest2lem  23128  ordtrest2  23129  leordtvallem1  23135  leordtvallem2  23136  cnclsi  23197  ordtt1  23304  cmpsub  23325  connsub  23346  cnconn  23347  nconnsubb  23348  connsubclo  23349  1stcfb  23370  kgentopon  23463  ptbasfi  23506  ptclsg  23540  dfac14lem  23542  xkoccn  23544  txcnmpt  23549  txtube  23565  xkoptsub  23579  xkopt  23580  kqsat  23656  kqcldsat  23658  ordthmeolem  23726  fbasrn  23809  trfil1  23811  trfil2  23812  trufil  23835  qustgphaus  24048  trust  24154  metustfbas  24482  cfilucfil  24484  xrsmopn  24738  lebnumii  24902  iscmet3  25230  resscdrg  25295  cmmbl  25472  voliunlem3  25490  uniioombllem4  25524  mbflimsup  25604  0plef  25610  0pledm  25611  itg1ge0  25624  mbfi1fseqlem5  25657  itg2addlem  25696  dvcmulf  25885  lhop1  25956  lhop2  25957  efopn  26604  wilthlem2  27016  ex-in  30416  cmcmlem  31582  pjvec  31687  pjocvec  31688  ssmd2  32303  mdslmd4i  32324  chirredlem2  32382  chirredlem3  32383  dmdbr7ati  32415  difuncomp  32544  xppreima  32638  suppovss  32673  fressupp  32680  gtiso  32693  preiman0  32702  fsuppcurry1  32718  fsuppcurry2  32719  resf1o  32724  elrgspnsubrunlem2  33226  elrspunidl  33404  ply1degltdimlem  33646  fldgenfldext  33692  rspectopn  33891  prsss  33940  ordtrestNEW  33945  ordtrest2NEWlem  33946  ordtrest2NEW  33947  lmxrge0  33976  carsggect  34342  probdsb  34446  totprobd  34450  cndprobtot  34460  orvcelval  34493  ballotlemfmpn  34519  signsplypnf  34574  signsply0  34575  dfon2lem4  35839  neibastop3  36417  weiunfrlem  36519  bj-restsnss  37138  bj-ismoored2  37163  bj-inexeqex  37209  bj-idreseq  37217  topdifinfeq  37405  poimirlem3  37673  poimirlem9  37679  mblfinlem3  37709  mblfinlem4  37710  itg2addnclem2  37722  blssp  37806  sstotbnd2  37824  lcvexchlem1  39143  lcvexchlem4  39146  glbconN  39486  pmapglb2N  39880  pmapglb2xN  39881  2polssN  40024  polatN  40040  osumcllem1N  40065  osumcllem9N  40073  pexmidlem6N  40084  diarnN  41238  dihmeetlem11N  41426  dochexmidlem6  41574  lclkrlem2r  41633  mapdunirnN  41759  fsuppssindlem2  42700  prjcrv0  42741  ofoafg  43461  harval3  43645  rfovcnvf1od  44111  fsovcnvlem  44120  ntrneifv3  44189  ntrneifv4  44192  clsneifv3  44217  clsneifv4  44218  neicvgfv  44228  k0004lem2  44255  wnefimgd  44268  inabs3  45167  stoweidlem50  46162  sge0iunmptlemre  46527  caratheodorylem1  46638  smfconst  46861  fresfo  47162  funfocofob  47192  grimuhgr  48001  restclsseplem  49029  incat  49716