Theorem dfss 3925

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

Assertion

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

Proof of Theorem dfss

Step	Hyp	Ref	Expression
1		dfss2 3924	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2		eqcom 2770	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 ↔ 𝐴 = (𝐴 ∩ 𝐵))
3	1, 2	bitri 278	1 ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 = (𝐴 ∩ 𝐵))

Syntax hints:   ↔ wb 209   = wceq 1570   ∩ cin 3905   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1105  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-in 3913  df-ss 3923

This theorem is referenced by:  iinrab2  5035  wefrc  5657  cnvcnv  6192  ordtri2or3  6465  onelini  6482  funimass1  6620  sbthlem5  9080  dmaddpi  10876  dmmulpi  10877  smndex1bas  18969  restcldi  23311  cmpsublem  23537  ustuqtop5  24383  tgioo  24934  cphsscph  25391  mdbr3  32630  mdbr4  32631  ssmd1  32644  xrge00  33315  esumpfinvallem  34445  measxun2  34581  eulerpartgbij  34743  reprfz1  34992  tr0elw  36976  tr0el  36977  bj-ismooredr2  37733  bndss  38418  redundss3  39342  dfrcl2  44383  isotone2  44758  wfac8prim  45694  restuni4  45822  fourierdlem93  46896  sge0resplit  47103  mbfresmf  47436