Theorem dfss 3921

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

Assertion

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

Proof of Theorem dfss

Step	Hyp	Ref	Expression
1		dfss2 3920	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2		eqcom 2768	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 ↔ 𝐴 = (𝐴 ∩ 𝐵))
3	1, 2	bitri 277	1 ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 = (𝐴 ∩ 𝐵))

Syntax hints:   ↔ wb 208   = wceq 1559   ∩ cin 3901   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-3an 1099  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-in 3909  df-ss 3919

This theorem is referenced by:  iinrab2  5024  wefrc  5637  cnvcnv  6172  ordtri2or3  6442  onelini  6459  funimass1  6597  sbthlem5  9056  dmaddpi  10841  dmmulpi  10842  smndex1bas  18933  restcldi  23220  cmpsublem  23446  ustuqtop5  24292  tgioo  24843  cphsscph  25300  mdbr3  32456  mdbr4  32457  ssmd1  32470  xrge00  33152  esumpfinvallem  34331  measxun2  34467  eulerpartgbij  34629  reprfz1  34878  tr0elw  36804  tr0el  36805  bj-ismooredr2  37560  bndss  38245  redundss3  39171  dfrcl2  44210  isotone2  44585  wfac8prim  45538  restuni4  45659  fourierdlem93  46733  sge0resplit  46940  mbfresmf  47273