Theorem dfss 3965

Description: Variant of subclass definition df-ss 3964. (Contributed by NM, 21-Jun-1993.)

Assertion

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

Proof of Theorem dfss

Step	Hyp	Ref	Expression
1		df-ss 3964	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2		eqcom 2735	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 ↔ 𝐴 = (𝐴 ∩ 𝐵))
3	1, 2	bitri 275	1 ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 = (𝐴 ∩ 𝐵))

Syntax hints:   ↔ wb 205   = wceq 1534   ∩ cin 3946   ⊆ wss 3947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-cleq 2720  df-ss 3964

This theorem is referenced by:  dfss2  3967  iinrab2  5073  wefrc  5672  cnvcnv  6196  ordtri2or3  6469  onelini  6487  funimass1  6635  sbthlem5  9111  dmaddpi  10913  dmmulpi  10914  smndex1bas  18857  restcldi  23076  cmpsublem  23302  ustuqtop5  24149  tgioo  24711  cphsscph  25178  mdbr3  32106  mdbr4  32107  ssmd1  32120  xrge00  32742  esumpfinvallem  33693  measxun2  33829  eulerpartgbij  33992  reprfz1  34256  bj-ismooredr2  36589  bndss  37259  redundss3  38100  dfrcl2  43104  isotone2  43479  restuni4  44487  fourierdlem93  45587  sge0resplit  45794  mbfresmf  46127