Theorem dfss 3917

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

Assertion

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

Proof of Theorem dfss

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

Syntax hints:   ↔ wb 206   = wceq 1541   ∩ cin 3897   ⊆ wss 3898

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 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-in 3905  df-ss 3915

This theorem is referenced by:  iinrab2  5022  wefrc  5615  cnvcnv  6146  ordtri2or3  6415  onelini  6432  funimass1  6570  sbthlem5  9013  dmaddpi  10790  dmmulpi  10791  smndex1bas  18818  restcldi  23091  cmpsublem  23317  ustuqtop5  24163  tgioo  24714  cphsscph  25181  mdbr3  32281  mdbr4  32282  ssmd1  32295  xrge00  33004  esumpfinvallem  34110  measxun2  34246  eulerpartgbij  34408  reprfz1  34660  bj-ismooredr2  37177  bndss  37849  redundss3  38747  dfrcl2  43794  isotone2  44169  wfac8prim  45122  restuni4  45245  fourierdlem93  46324  sge0resplit  46531  mbfresmf  46864