Theorem sseqin2 4186

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∩ cin 3913   ⊆ wss 3914

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-in 3921  df-ss 3931

This theorem is referenced by:  dfss4  4232  rintn0  5073  resabs1  5977  resima2  5987  xpssres  5989  mptimass  6044  rescnvcnv  6177  sspred  6283  trpred  6304  predres  6312  onfr  6371  ordtri2or3  6434  fndmdif  7014  fimacnvinrn2  7044  fveqressseq  7051  sorpssin  7707  cnvoprab  8039  frpoins3xpg  8119  frpoins3xp3g  8120  xpord3pred  8131  fsuppeq  8154  fsuppeqg  8155  frrlem4  8268  fiint  9277  fiintOLD  9278  infxpenlem  9966  acndom2  10007  ackbij1lem2  10173  isf34lem5  10331  fpwwe2  10596  uzin  12833  iooval2  13339  fzval2  13471  leiso  14424  fz1isolem  14426  isercolllem3  15633  incexc  15803  bitsinv1  16412  bitsinvp1  16419  bitsshft  16445  dfphi2  16744  ressbas  17206  ressress  17217  ressabs  17218  psssdm  18541  sylow3lem2  19558  gsumxp  19906  dprdsn  19968  ablfac1eu  20005  pgpfac1lem5  20011  ablfaclem3  20019  ocv1  21588  resttopon  23048  restabs  23052  restopnb  23062  restperf  23071  ordtbas  23079  ordtrest2lem  23090  ordtrest2  23091  leordtvallem1  23097  leordtvallem2  23098  cnclsi  23159  ordtt1  23266  cmpsub  23287  connsub  23308  cnconn  23309  nconnsubb  23310  connsubclo  23311  1stcfb  23332  kgentopon  23425  ptbasfi  23468  ptclsg  23502  dfac14lem  23504  xkoccn  23506  txcnmpt  23511  txtube  23527  xkoptsub  23541  xkopt  23542  kqsat  23618  kqcldsat  23620  ordthmeolem  23688  fbasrn  23771  trfil1  23773  trfil2  23774  trufil  23797  qustgphaus  24010  trust  24117  metustfbas  24445  cfilucfil  24447  xrsmopn  24701  lebnumii  24865  iscmet3  25193  resscdrg  25258  cmmbl  25435  voliunlem3  25453  uniioombllem4  25487  mbflimsup  25567  0plef  25573  0pledm  25574  itg1ge0  25587  mbfi1fseqlem5  25620  itg2addlem  25659  dvcmulf  25848  lhop1  25919  lhop2  25920  efopn  26567  wilthlem2  26979  ex-in  30354  cmcmlem  31520  pjvec  31625  pjocvec  31626  ssmd2  32241  mdslmd4i  32262  chirredlem2  32320  chirredlem3  32321  dmdbr7ati  32353  difuncomp  32482  xppreima  32569  suppovss  32604  fressupp  32611  gtiso  32624  preiman0  32633  fsuppcurry1  32648  fsuppcurry2  32649  resf1o  32653  elrgspnsubrunlem2  33199  elrspunidl  33399  ply1degltdimlem  33618  fldgenfldext  33663  rspectopn  33857  prsss  33906  ordtrestNEW  33911  ordtrest2NEWlem  33912  ordtrest2NEW  33913  lmxrge0  33942  carsggect  34309  probdsb  34413  totprobd  34417  cndprobtot  34427  orvcelval  34460  ballotlemfmpn  34486  signsplypnf  34541  signsply0  34542  dfon2lem4  35774  neibastop3  36350  weiunfrlem  36452  bj-restsnss  37071  bj-ismoored2  37096  bj-inexeqex  37142  bj-idreseq  37150  topdifinfeq  37338  poimirlem3  37617  poimirlem9  37623  mblfinlem3  37653  mblfinlem4  37654  itg2addnclem2  37666  blssp  37750  sstotbnd2  37768  lcvexchlem1  39027  lcvexchlem4  39030  glbconN  39370  glbconNOLD  39371  pmapglb2N  39765  pmapglb2xN  39766  2polssN  39909  polatN  39925  osumcllem1N  39950  osumcllem9N  39958  pexmidlem6N  39969  diarnN  41123  dihmeetlem11N  41311  dochexmidlem6  41459  lclkrlem2r  41518  mapdunirnN  41644  fsuppssindlem2  42580  prjcrv0  42621  ofoafg  43343  harval3  43527  rfovcnvf1od  43993  fsovcnvlem  44002  ntrneifv3  44071  ntrneifv4  44074  clsneifv3  44099  clsneifv4  44100  neicvgfv  44110  k0004lem2  44137  wnefimgd  44150  inabs3  45050  stoweidlem50  46048  sge0iunmptlemre  46413  caratheodorylem1  46524  smfconst  46747  fresfo  47049  funfocofob  47079  grimuhgr  47887  restclsseplem  48903  incat  49590