Theorem dfss 3950

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

Assertion

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

Proof of Theorem dfss

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∩ cin 3930   ⊆ wss 3931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-in 3938  df-ss 3948

This theorem is referenced by:  iinrab2  5051  wefrc  5653  cnvcnv  6186  ordtri2or3  6459  onelini  6477  funimass1  6623  sbthlem5  9106  dmaddpi  10909  dmmulpi  10910  smndex1bas  18889  restcldi  23116  cmpsublem  23342  ustuqtop5  24189  tgioo  24740  cphsscph  25208  mdbr3  32283  mdbr4  32284  ssmd1  32297  xrge00  33012  esumpfinvallem  34110  measxun2  34246  eulerpartgbij  34409  reprfz1  34661  bj-ismooredr2  37133  bndss  37815  redundss3  38651  dfrcl2  43665  isotone2  44040  wfac8prim  44994  restuni4  45112  fourierdlem93  46195  sge0resplit  46402  mbfresmf  46735