Theorem sseqin2 4046

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 3812	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2		incom 4034	. . 3 ⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴)
3	2	eqeq1i 2830	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 ↔ (𝐵 ∩ 𝐴) = 𝐴)
4	1, 3	bitri 267	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∩ 𝐴) = 𝐴)

Syntax hints:   ↔ wb 198   = wceq 1656   ∩ cin 3797   ⊆ wss 3798

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-v 3416  df-in 3805  df-ss 3812

This theorem is referenced by:  dfss4  4090  rintn0  4842  resabs1  5667  resima2  5672  xpssres  5673  rescnvcnv  5842  sspred  5932  onfr  6006  ordtri2or3  6064  fndmdif  6575  fimacnvinrn2  6603  fveqressseq  6609  sorpssin  7210  predon  7257  omsinds  7350  cnvoprab  7497  frnsuppeq  7576  wfrlem4  7688  wfrlem4OLD  7689  fiint  8512  infxpenlem  9156  acndom2  9197  ackbij1lem2  9365  isf34lem5  9522  fpwwe2  9787  uzin  12009  iooval2  12503  fzval2  12629  leiso  13539  fz1isolem  13541  isercolllem3  14781  incexc  14950  bitsinv1  15544  bitsinvp1  15551  bitsshft  15577  dfphi2  15857  ressbas  16300  ressress  16309  ressabs  16310  psssdm  17576  sylow3lem2  18401  gsumxp  18735  dprdsn  18796  ablfac1eu  18833  pgpfac1lem5  18839  ablfaclem3  18847  ocv1  20393  resttopon  21343  restabs  21347  restopnb  21357  restperf  21366  ordtbas  21374  ordtrest2lem  21385  ordtrest2  21386  leordtvallem1  21392  leordtvallem2  21393  cnclsi  21454  ordtt1  21561  cmpsub  21581  connsub  21602  cnconn  21603  nconnsubb  21604  connsubclo  21605  1stcfb  21626  kgentopon  21719  ptbasfi  21762  ptclsg  21796  dfac14lem  21798  xkoccn  21800  txcnmpt  21805  txtube  21821  xkoptsub  21835  xkopt  21836  kqsat  21912  kqcldsat  21914  ordthmeolem  21982  fbasrn  22065  trfil1  22067  trfil2  22068  trufil  22091  qustgphaus  22303  trust  22410  metustfbas  22739  cfilucfil  22741  xrsmopn  22992  lebnumii  23142  iscmet3  23468  resscdrg  23533  cmmbl  23707  voliunlem3  23725  uniioombllem4  23759  mbflimsup  23839  0plef  23845  0pledm  23846  itg1ge0  23859  mbfi1fseqlem5  23892  itg2addlem  23931  dvcmulf  24114  lhop1  24183  lhop2  24184  efopn  24810  wilthlem2  25215  ex-in  27836  cmcmlem  29001  pjvec  29106  pjocvec  29107  ssmd2  29722  mdslmd4i  29743  chirredlem2  29801  chirredlem3  29802  dmdbr7ati  29834  difuncomp  29913  xppreima  29994  gtiso  30022  resf1o  30049  prsss  30503  ordtrestNEW  30508  ordtrest2NEWlem  30509  ordtrest2NEW  30510  lmxrge0  30539  carsggect  30921  probdsb  31026  totprobd  31030  cndprobtot  31040  orvcelval  31072  ballotlemfmpn  31098  signsplypnf  31170  signsply0  31171  dfon2lem4  32224  frrlem4  32317  neibastop3  32890  bj-restsnss  33554  bj-ismoored2  33581  bj-ismooredr2  33583  topdifinfeq  33738  poimirlem3  33951  poimirlem9  33957  mblfinlem3  33987  mblfinlem4  33988  itg2addnclem2  34000  blssp  34089  sstotbnd2  34110  lcvexchlem1  35104  lcvexchlem4  35107  glbconN  35447  pmapglb2N  35841  pmapglb2xN  35842  2polssN  35985  polatN  36001  osumcllem1N  36026  osumcllem9N  36034  pexmidlem6N  36045  diarnN  37199  dihmeetlem11N  37387  dochexmidlem6  37535  lclkrlem2r  37594  mapdunirnN  37720  rfovcnvf1od  39133  fsovcnvlem  39142  ntrneifv3  39215  ntrneifv4  39218  clsneifv3  39243  clsneifv4  39244  neicvgfv  39254  k0004lem2  39281  wnefimgd  39295  inabs3  40036  mptima2  40252  stoweidlem50  41055  sge0iunmptlemre  41417  caratheodorylem1  41528  smfconst  41746