Theorem dfss 3901

Description: Variant of subclass definition df-ss 3900. (Contributed by NM, 21-Jun-1993.)

Assertion

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

Proof of Theorem dfss

Step	Hyp	Ref	Expression
1		df-ss 3900	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2		eqcom 2745	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 ↔ 𝐴 = (𝐴 ∩ 𝐵))
3	1, 2	bitri 274	1 ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 = (𝐴 ∩ 𝐵))

Syntax hints:   ↔ wb 205   = wceq 1539   ∩ cin 3882   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-ss 3900

This theorem is referenced by:  dfss2  3903  dfss2OLD  3904  iinrab2  4995  wefrc  5574  cnvcnv  6084  ordtri2or3  6348  onelini  6363  funimass1  6500  sbthlem5  8827  dmaddpi  10577  dmmulpi  10578  smndex1bas  18460  restcldi  22232  cmpsublem  22458  ustuqtop5  23305  tgioo  23865  cphsscph  24320  mdbr3  30560  mdbr4  30561  ssmd1  30574  xrge00  31197  esumpfinvallem  31942  measxun2  32078  eulerpartgbij  32239  reprfz1  32504  bj-ismooredr2  35208  bndss  35871  redundss3  36668  dfrcl2  41171  isotone2  41548  restuni4  42559  fourierdlem93  43630  sge0resplit  43834  mbfresmf  44162