Theorem sseqin2 4123

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 4097	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2		ineqcom 4110	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 ↔ (𝐵 ∩ 𝐴) = 𝐴)
3	1, 2	bitri 278	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∩ 𝐴) = 𝐴)

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ⊆ wss 3900   ∩ cin 4092

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-ss 3901  df-in 4094

This theorem is used by:  dfss4  4217  rintn0  5072  resabs1  6009  xpssres  6019  resima2  6069  mptimass  6083  rescnvcnv  6218  sspred  6331  trpred  6352  predres  6360  onfr  6420  ordtri2or3  6483  fndmdif  7064  fimacnvinrn2  7096  fveqressseq  7103  sorpssin  7771  cnvoprab  8096  frpoins3xpg  8184  frpoins3xp3g  8185  xpord3pred  8196  fsuppeq  8220  fsuppeqg  8221  frrlem4  8335  fiint  9346  infxpenlem  10119  acndom2  10160  ackbij1lem2  10325  isf34lem5  10483  fpwwe2  10755  uzin  13028  iooval2  13536  fzval2  13669  leiso  14631  fz1isolem  14633  isercolllem3  15863  incexc  16035  bitsinv1  16641  bitsinvp1  16648  bitsshft  16674  dfphi2  16980  ressbas  17443  ressress  17454  ressabs  17455  psssdm  18785  sylow3lem2  19872  gsumxp  20220  dprdsn  20282  ablfac1eu  20319  pgpfac1lem5  20325  ablfaclem3  20333  ocv1  22015  resttopon  23509  restabs  23513  restopnb  23523  restperf  23532  ordtbas  23540  ordtrest2lem  23551  ordtrest2  23552  leordtvallem1  23558  leordtvallem2  23559  cnclsi  23620  ordtt1  23727  cmpsub  23748  connsub  23769  cnconn  23770  nconnsubb  23771  connsubclo  23772  1stcfb  23793  kgentopon  23887  ptbasfi  23930  ptclsg  23964  dfac14lem  23966  xkoccn  23968  txcnmpt  23973  txtube  23989  xkoptsub  24003  xkopt  24004  kqsat  24080  kqcldsat  24082  ordthmeolem  24150  fbasrn  24233  trfil1  24235  trfil2  24236  trufil  24259  qustgphaus  24472  trust  24578  metustfbas  24906  cfilucfil  24908  xrsmopn  25162  lebnumii  25317  iscmet3  25644  resscdrg  25709  cmmbl  25885  voliunlem3  25903  uniioombllem4  25937  mbflimsup  26017  0plef  26023  0pledm  26024  itg1ge0  26037  mbfi1fseqlem5  26070  itg2addlem  26109  dvcmulf  26295  lhop1  26364  lhop2  26365  efopn  27016  wilthlem2  27426  ex-in  31056  cmcmlem  32223  pjvec  32328  pjocvec  32329  ssmd2  32944  mdslmd4i  32965  chirredlem2  33023  chirredlem3  33024  dmdbr7ati  33056  difuncomp  33220  xppreima  33311  partfun2  33341  suppovss  33345  fressupp  33352  gtiso  33365  preiman0  33374  fsuppcurry1  33386  fsuppcurry2  33387  resf1o  33392  elrgspnsubrunlem2  33879  elrspunidl  34048  ply1degltdimlem  34324  fldgenfldext  34370  rspectopn  34569  prsss  34618  ordtrestNEW  34623  ordtrest2NEWlem  34624  ordtrest2NEW  34625  lmxrge0  34654  carsggect  35020  probdsb  35124  totprobd  35128  cndprobtot  35138  orvcelval  35171  ballotlemfmpn  35197  signsplypnf  35249  signsply0  35250  j0ltalephlem  36007  dfon2lem4  36726  neibastop3  37328  weiunfrlem  37430  bj-restsnss  38195  bj-ismoored2  38220  bj-inexeqex  38267  bj-idreseq  38275  topdifinfeq  38465  poimirlem3  38733  poimirlem9  38739  mblfinlem3  38769  mblfinlem4  38770  itg2addnclem2  38782  blssp  38882  sstotbnd2  38900  lcvexchlem1  40283  lcvexchlem4  40286  glbconN  40626  pmapglb2N  41020  pmapglb2xN  41021  2polssN  41164  polatN  41180  osumcllem1N  41205  osumcllem9N  41213  pexmidlem6N  41224  diarnN  42378  dihmeetlem11N  42566  dochexmidlem6  42714  lclkrlem2r  42773  mapdunirnN  42899  fsuppssindlem2  43813  prjcrv0  43862  ofoafg  44548  harval3  44731  rfovcnvf1od  45196  fsovcnvlem  45205  ntrneifv3  45274  ntrneifv4  45277  clsneifv3  45302  clsneifv4  45303  neicvgfv  45313  k0004lem2  45340  wnefimgd  45353  inabs3  46278  stoweidlem50  47265  sge0iunmptlemre  47630  caratheodorylem1  47741  smfconst  47964  fresfo  48323  funfocofob  48353  grimuhgr  49190  restclsseplem  50234  incat  50944  parhomco2  50965  parhomco  50966  parcatid2  50968  parcatid  50969  parmapco2  50977  parmapco  50978