Theorem dfss 3920

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

Assertion

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

Proof of Theorem dfss

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

Syntax hints:   ↔ wb 206   = wceq 1541   ∩ cin 3900   ⊆ wss 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-in 3908  df-ss 3918

This theorem is referenced by:  iinrab2  5025  wefrc  5618  cnvcnv  6150  ordtri2or3  6419  onelini  6436  funimass1  6574  sbthlem5  9019  dmaddpi  10801  dmmulpi  10802  smndex1bas  18831  restcldi  23117  cmpsublem  23343  ustuqtop5  24189  tgioo  24740  cphsscph  25207  mdbr3  32372  mdbr4  32373  ssmd1  32386  xrge00  33096  esumpfinvallem  34231  measxun2  34367  eulerpartgbij  34529  reprfz1  34781  bj-ismooredr2  37315  bndss  37987  redundss3  38885  dfrcl2  43915  isotone2  44290  wfac8prim  45243  restuni4  45365  fourierdlem93  46443  sge0resplit  46650  mbfresmf  46983