Theorem dfss 3905

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

Assertion

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

Proof of Theorem dfss

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

Syntax hints:   ↔ wb 205   = wceq 1539   ∩ cin 3886   ⊆ wss 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-ss 3904

This theorem is referenced by:  dfss2  3907  dfss2OLD  3908  iinrab2  4999  wefrc  5583  cnvcnv  6095  ordtri2or3  6363  onelini  6378  funimass1  6516  sbthlem5  8874  dmaddpi  10646  dmmulpi  10647  smndex1bas  18545  restcldi  22324  cmpsublem  22550  ustuqtop5  23397  tgioo  23959  cphsscph  24415  mdbr3  30659  mdbr4  30660  ssmd1  30673  xrge00  31295  esumpfinvallem  32042  measxun2  32178  eulerpartgbij  32339  reprfz1  32604  bj-ismooredr2  35281  bndss  35944  redundss3  36741  dfrcl2  41282  isotone2  41659  restuni4  42670  fourierdlem93  43740  sge0resplit  43944  mbfresmf  44275