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 2747	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 ↔ 𝐴 = (𝐴 ∩ 𝐵))
3	1, 2	bitri 276	1 ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 = (𝐴 ∩ 𝐵))

Syntax hints:   ↔ wb 207   = wceq 1547   ∩ cin 3889   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1094  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-in 3897  df-ss 3907

This theorem is referenced by:  iinrab2  5006  wefrc  5619  cnvcnv  6150  ordtri2or3  6419  onelini  6436  funimass1  6574  sbthlem5  9026  dmaddpi  10811  dmmulpi  10812  smndex1bas  18875  restcldi  23163  cmpsublem  23389  ustuqtop5  24235  tgioo  24786  cphsscph  25243  mdbr3  32393  mdbr4  32394  ssmd1  32407  xrge00  33100  esumpfinvallem  34265  measxun2  34401  eulerpartgbij  34563  reprfz1  34815  tr0elw  36719  tr0el  36720  bj-ismooredr2  37475  bndss  38160  redundss3  39086  dfrcl2  44125  isotone2  44500  wfac8prim  45453  restuni4  45575  fourierdlem93  46649  sge0resplit  46856  mbfresmf  47189