Theorem dfss 3908

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

Assertion

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

Proof of Theorem dfss

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

Syntax hints:   ↔ wb 206   = wceq 1542   ∩ cin 3888   ⊆ wss 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-in 3896  df-ss 3906

This theorem is referenced by:  iinrab2  5012  wefrc  5625  cnvcnv  6156  ordtri2or3  6425  onelini  6442  funimass1  6580  sbthlem5  9029  dmaddpi  10813  dmmulpi  10814  smndex1bas  18877  restcldi  23138  cmpsublem  23364  ustuqtop5  24210  tgioo  24761  cphsscph  25218  mdbr3  32368  mdbr4  32369  ssmd1  32382  xrge00  33074  esumpfinvallem  34218  measxun2  34354  eulerpartgbij  34516  reprfz1  34768  tr0elw  36666  tr0el  36667  bj-ismooredr2  37422  bndss  38107  redundss3  39033  dfrcl2  44101  isotone2  44476  wfac8prim  45429  restuni4  45551  fourierdlem93  46627  sge0resplit  46834  mbfresmf  47167