Theorem dfss 3995

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

Assertion

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

Proof of Theorem dfss

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

Syntax hints:   ↔ wb 206   = wceq 1537   ∩ cin 3975   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-in 3983  df-ss 3993

This theorem is referenced by:  iinrab2  5093  wefrc  5694  cnvcnv  6223  ordtri2or3  6495  onelini  6513  funimass1  6660  sbthlem5  9153  dmaddpi  10959  dmmulpi  10960  smndex1bas  18941  restcldi  23202  cmpsublem  23428  ustuqtop5  24275  tgioo  24837  cphsscph  25304  mdbr3  32329  mdbr4  32330  ssmd1  32343  xrge00  32998  esumpfinvallem  34038  measxun2  34174  eulerpartgbij  34337  reprfz1  34601  bj-ismooredr2  37076  bndss  37746  redundss3  38584  dfrcl2  43636  isotone2  44011  restuni4  45023  fourierdlem93  46120  sge0resplit  46327  mbfresmf  46660