Theorem dfss 3970

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

Assertion

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

Proof of Theorem dfss

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∩ cin 3950   ⊆ wss 3951

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-in 3958  df-ss 3968

This theorem is referenced by:  iinrab2  5070  wefrc  5679  cnvcnv  6212  ordtri2or3  6484  onelini  6502  funimass1  6648  sbthlem5  9127  dmaddpi  10930  dmmulpi  10931  smndex1bas  18919  restcldi  23181  cmpsublem  23407  ustuqtop5  24254  tgioo  24817  cphsscph  25285  mdbr3  32316  mdbr4  32317  ssmd1  32330  xrge00  33017  esumpfinvallem  34075  measxun2  34211  eulerpartgbij  34374  reprfz1  34639  bj-ismooredr2  37111  bndss  37793  redundss3  38629  dfrcl2  43687  isotone2  44062  wfac8prim  45019  restuni4  45126  fourierdlem93  46214  sge0resplit  46421  mbfresmf  46754