Theorem sseqin2 4244

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

Syntax hints:   ↔ wb 206   = wceq 1537   ∩ cin 3975   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-in 3983  df-ss 3993

This theorem is referenced by:  dfss4  4288  rintn0  5132  resabs1  6036  resima2  6045  xpssres  6047  mptimass  6102  rescnvcnv  6235  sspred  6341  trpred  6363  predres  6371  onfr  6434  ordtri2or3  6495  fndmdif  7075  fimacnvinrn2  7106  fveqressseq  7113  sorpssin  7766  predonOLD  7822  omsindsOLD  7925  cnvoprab  8101  frpoins3xpg  8181  frpoins3xp3g  8182  xpord3pred  8193  fsuppeq  8216  fsuppeqg  8217  frrlem4  8330  wfrlem4OLD  8368  fiint  9394  fiintOLD  9395  infxpenlem  10082  acndom2  10123  ackbij1lem2  10289  isf34lem5  10447  fpwwe2  10712  uzin  12943  iooval2  13440  fzval2  13570  leiso  14508  fz1isolem  14510  isercolllem3  15715  incexc  15885  bitsinv1  16488  bitsinvp1  16495  bitsshft  16521  dfphi2  16821  ressbas  17293  ressbasOLD  17294  ressress  17307  ressabs  17308  psssdm  18652  sylow3lem2  19670  gsumxp  20018  dprdsn  20080  ablfac1eu  20117  pgpfac1lem5  20123  ablfaclem3  20131  ocv1  21720  resttopon  23190  restabs  23194  restopnb  23204  restperf  23213  ordtbas  23221  ordtrest2lem  23232  ordtrest2  23233  leordtvallem1  23239  leordtvallem2  23240  cnclsi  23301  ordtt1  23408  cmpsub  23429  connsub  23450  cnconn  23451  nconnsubb  23452  connsubclo  23453  1stcfb  23474  kgentopon  23567  ptbasfi  23610  ptclsg  23644  dfac14lem  23646  xkoccn  23648  txcnmpt  23653  txtube  23669  xkoptsub  23683  xkopt  23684  kqsat  23760  kqcldsat  23762  ordthmeolem  23830  fbasrn  23913  trfil1  23915  trfil2  23916  trufil  23939  qustgphaus  24152  trust  24259  metustfbas  24591  cfilucfil  24593  xrsmopn  24853  lebnumii  25017  iscmet3  25346  resscdrg  25411  cmmbl  25588  voliunlem3  25606  uniioombllem4  25640  mbflimsup  25720  0plef  25726  0pledm  25727  itg1ge0  25740  mbfi1fseqlem5  25774  itg2addlem  25813  dvcmulf  26002  lhop1  26073  lhop2  26074  efopn  26718  wilthlem2  27130  ex-in  30457  cmcmlem  31623  pjvec  31728  pjocvec  31729  ssmd2  32344  mdslmd4i  32365  chirredlem2  32423  chirredlem3  32424  dmdbr7ati  32456  difuncomp  32576  xppreima  32664  suppovss  32697  fressupp  32700  gtiso  32712  preiman0  32721  fsuppcurry1  32739  fsuppcurry2  32740  resf1o  32744  elrspunidl  33421  ply1degltdimlem  33635  fldgenfldext  33678  rspectopn  33813  prsss  33862  ordtrestNEW  33867  ordtrest2NEWlem  33868  ordtrest2NEW  33869  lmxrge0  33898  carsggect  34283  probdsb  34387  totprobd  34391  cndprobtot  34401  orvcelval  34433  ballotlemfmpn  34459  signsplypnf  34527  signsply0  34528  dfon2lem4  35750  neibastop3  36328  weiunfrlem  36430  bj-restsnss  37049  bj-ismoored2  37074  bj-inexeqex  37120  bj-idreseq  37128  topdifinfeq  37316  poimirlem3  37583  poimirlem9  37589  mblfinlem3  37619  mblfinlem4  37620  itg2addnclem2  37632  blssp  37716  sstotbnd2  37734  lcvexchlem1  38990  lcvexchlem4  38993  glbconN  39333  glbconNOLD  39334  pmapglb2N  39728  pmapglb2xN  39729  2polssN  39872  polatN  39888  osumcllem1N  39913  osumcllem9N  39921  pexmidlem6N  39932  diarnN  41086  dihmeetlem11N  41274  dochexmidlem6  41422  lclkrlem2r  41481  mapdunirnN  41607  fsuppssindlem2  42547  prjcrv0  42588  ofoafg  43316  harval3  43500  rfovcnvf1od  43966  fsovcnvlem  43975  ntrneifv3  44044  ntrneifv4  44047  clsneifv3  44072  clsneifv4  44073  neicvgfv  44083  k0004lem2  44110  wnefimgd  44123  inabs3  44958  stoweidlem50  45971  sge0iunmptlemre  46336  caratheodorylem1  46447  smfconst  46670  fresfo  46963  funfocofob  46993  grimuhgr  47762  restclsseplem  48594