Theorem dfss 3982

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

Assertion

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

Proof of Theorem dfss

Step	Hyp	Ref	Expression
1		dfss2 3981	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2		eqcom 2742	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 ↔ 𝐴 = (𝐴 ∩ 𝐵))
3	1, 2	bitri 275	1 ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 = (𝐴 ∩ 𝐵))

Syntax hints:   ↔ wb 206   = wceq 1537   ∩ cin 3962   ⊆ wss 3963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-in 3970  df-ss 3980

This theorem is referenced by:  iinrab2  5075  wefrc  5683  cnvcnv  6214  ordtri2or3  6486  onelini  6504  funimass1  6650  sbthlem5  9126  dmaddpi  10928  dmmulpi  10929  smndex1bas  18932  restcldi  23197  cmpsublem  23423  ustuqtop5  24270  tgioo  24832  cphsscph  25299  mdbr3  32326  mdbr4  32327  ssmd1  32340  xrge00  33000  esumpfinvallem  34055  measxun2  34191  eulerpartgbij  34354  reprfz1  34618  bj-ismooredr2  37093  bndss  37773  redundss3  38610  dfrcl2  43664  isotone2  44039  restuni4  45061  fourierdlem93  46155  sge0resplit  46362  mbfresmf  46695