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

Syntax hints:   ↔ wb 206   = wceq 1541   ∩ cin 3901   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-in 3909  df-ss 3919

This theorem is referenced by:  iinrab2  5018  wefrc  5610  cnvcnv  6139  ordtri2or3  6408  onelini  6425  funimass1  6563  sbthlem5  9004  dmaddpi  10781  dmmulpi  10782  smndex1bas  18814  restcldi  23089  cmpsublem  23315  ustuqtop5  24161  tgioo  24712  cphsscph  25179  mdbr3  32275  mdbr4  32276  ssmd1  32289  xrge00  32993  esumpfinvallem  34085  measxun2  34221  eulerpartgbij  34383  reprfz1  34635  bj-ismooredr2  37150  bndss  37832  redundss3  38671  dfrcl2  43713  isotone2  44088  wfac8prim  45041  restuni4  45164  fourierdlem93  46243  sge0resplit  46450  mbfresmf  46783