Theorem dfss 3966

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

Assertion

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

Proof of Theorem dfss

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

Syntax hints:   ↔ wb 205   = wceq 1541   ∩ cin 3947   ⊆ wss 3948

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-ss 3965

This theorem is referenced by:  dfss2  3968  dfss2OLD  3969  iinrab2  5073  wefrc  5670  cnvcnv  6191  ordtri2or3  6464  onelini  6482  funimass1  6630  sbthlem5  9089  dmaddpi  10887  dmmulpi  10888  smndex1bas  18789  restcldi  22684  cmpsublem  22910  ustuqtop5  23757  tgioo  24319  cphsscph  24775  mdbr3  31588  mdbr4  31589  ssmd1  31602  xrge00  32225  esumpfinvallem  33141  measxun2  33277  eulerpartgbij  33440  reprfz1  33705  bj-ismooredr2  36083  bndss  36746  redundss3  37590  dfrcl2  42513  isotone2  42888  restuni4  43898  fourierdlem93  45000  sge0resplit  45207  mbfresmf  45540