Theorem dfss 3933

Description: Variant of subclass definition dfss2 3932. (Contributed by NM, 21-Jun-1993.)

Assertion

Ref	Expression
dfss	⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 = (𝐴 ∩ 𝐵))

Proof of Theorem dfss

Step	Hyp	Ref	Expression
1		dfss2 3932	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2		eqcom 2736	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 ↔ 𝐴 = (𝐴 ∩ 𝐵))
3	1, 2	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-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-in 3921  df-ss 3931

This theorem is referenced by:  iinrab2  5034  wefrc  5632  cnvcnv  6165  ordtri2or3  6434  onelini  6452  funimass1  6598  sbthlem5  9055  dmaddpi  10843  dmmulpi  10844  smndex1bas  18833  restcldi  23060  cmpsublem  23286  ustuqtop5  24133  tgioo  24684  cphsscph  25151  mdbr3  32226  mdbr4  32227  ssmd1  32240  xrge00  32953  esumpfinvallem  34064  measxun2  34200  eulerpartgbij  34363  reprfz1  34615  bj-ismooredr2  37098  bndss  37780  redundss3  38619  dfrcl2  43663  isotone2  44038  wfac8prim  44992  restuni4  45115  fourierdlem93  46197  sge0resplit  46404  mbfresmf  46737