Theorem dfss 3926

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

Assertion

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

Proof of Theorem dfss

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

Syntax hints:   ↔ wb 209   = wceq 1563   ∩ cin 3906   ⊆ wss 3907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-in 3914  df-ss 3924

This theorem is referenced by:  iinrab2  5029  wefrc  5645  cnvcnv  6181  ordtri2or3  6452  onelini  6469  funimass1  6607  sbthlem5  9067  dmaddpi  10863  dmmulpi  10864  smndex1bas  18956  restcldi  23287  cmpsublem  23513  ustuqtop5  24359  tgioo  24910  cphsscph  25367  mdbr3  32554  mdbr4  32555  ssmd1  32568  xrge00  33242  esumpfinvallem  34376  measxun2  34512  eulerpartgbij  34674  reprfz1  34923  tr0elw  36852  tr0el  36853  bj-ismooredr2  37607  bndss  38292  redundss3  39218  dfrcl2  44257  isotone2  44632  wfac8prim  45570  restuni4  45698  fourierdlem93  46772  sge0resplit  46979  mbfresmf  47312