Theorem dfss 3921

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

Assertion

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

Proof of Theorem dfss

Step	Hyp	Ref	Expression
1		dfss2 3920	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2		eqcom 2769	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 ↔ 𝐴 = (𝐴 ∩ 𝐵))
3	1, 2	bitri 278	1 ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 = (𝐴 ∩ 𝐵))

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ∩ cin 3901   ⊆ wss 3902

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-in 3909  df-ss 3919

This theorem is used by:  iinrab2  5032  wefrc  5653  cnvcnv  6189  ordtri2or3  6464  onelini  6481  funimass1  6619  sbthlem5  9093  dmaddpi  10903  dmmulpi  10904  smndex1bas  19024  restcldi  23404  cmpsublem  23630  ustuqtop5  24477  tgioo  25028  cphsscph  25485  mdbr3  32786  mdbr4  32787  ssmd1  32800  xrge00  33462  esumpfinvallem  34592  measxun2  34729  eulerpartgbij  34891  reprfz1  35140  tr0elw  37111  tr0el  37112  bj-ismooredr2  37868  bndss  38544  redundss3  39468  dfrcl2  44522  isotone2  44897  wfac8prim  45833  restuni4  45961  fourierdlem93  47035  sge0resplit  47242  mbfresmf  47575