Theorem dfss 3923

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

Assertion

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

Proof of Theorem dfss

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

Syntax hints:   ↔ wb 208   = wceq 1559   ∩ cin 3903   ⊆ wss 3904

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 3911  df-ss 3921

This theorem is referenced by:  iinrab2  5026  wefrc  5639  cnvcnv  6172  ordtri2or3  6442  onelini  6459  funimass1  6597  sbthlem5  9057  dmaddpi  10843  dmmulpi  10844  smndex1bas  18924  restcldi  23211  cmpsublem  23437  ustuqtop5  24283  tgioo  24834  cphsscph  25291  mdbr3  32444  mdbr4  32445  ssmd1  32458  xrge00  33151  esumpfinvallem  34330  measxun2  34466  eulerpartgbij  34628  reprfz1  34880  tr0elw  36797  tr0el  36798  bj-ismooredr2  37553  bndss  38238  redundss3  39164  dfrcl2  44203  isotone2  44578  wfac8prim  45531  restuni4  45652  fourierdlem93  46726  sge0resplit  46933  mbfresmf  47266