Theorem dfss 3555

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

Assertion

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

Proof of Theorem dfss

Step	Hyp	Ref	Expression
1		df-ss 3554	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2		eqcom 2617	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 ↔ 𝐴 = (𝐴 ∩ 𝐵))
3	1, 2	bitri 263	1 ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 = (𝐴 ∩ 𝐵))

Syntax hints:   ↔ wb 195   = wceq 1475   ∩ cin 3539   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603  df-ss 3554

This theorem is referenced by:  dfss2  3557  iinrab2  4519  wefrc  5032  cnvcnv  5505  ordtri2or3  5741  onelini  5756  funimass1  5885  sbthlem5  7959  dmaddpi  9591  dmmulpi  9592  restcldi  20787  cmpsublem  21012  ustuqtop5  21859  tgioo  22407  mdbr3  28540  mdbr4  28541  ssmd1  28554  xrge00  29017  esumpfinvallem  29463  measxun2  29600  eulerpartgbij  29761  bndss  32755  dfrcl2  36985  isotone2  37367  restuni4  38336  fourierdlem93  39092  sge0resplit  39299  mbfresmf  39626