Theorem dfss 3909

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

Assertion

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

Proof of Theorem dfss

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

Syntax hints:   ↔ wb 206   = wceq 1542   ∩ cin 3889   ⊆ wss 3890

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-in 3897  df-ss 3907

This theorem is referenced by:  iinrab2  5013  wefrc  5618  cnvcnv  6150  ordtri2or3  6419  onelini  6436  funimass1  6574  sbthlem5  9022  dmaddpi  10804  dmmulpi  10805  smndex1bas  18868  restcldi  23148  cmpsublem  23374  ustuqtop5  24220  tgioo  24771  cphsscph  25228  mdbr3  32383  mdbr4  32384  ssmd1  32397  xrge00  33089  esumpfinvallem  34234  measxun2  34370  eulerpartgbij  34532  reprfz1  34784  tr0elw  36682  tr0el  36683  bj-ismooredr2  37438  bndss  38121  redundss3  39047  dfrcl2  44119  isotone2  44494  wfac8prim  45447  restuni4  45569  fourierdlem93  46645  sge0resplit  46852  mbfresmf  47185