Theorem dfss 3927

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

Assertion

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

Proof of Theorem dfss

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

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

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 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-in 3915  df-ss 3925

This theorem is used by:  iinrab2  5039  wefrc  5660  cnvcnv  6195  ordtri2or3  6470  onelini  6487  funimass1  6625  sbthlem5  9089  dmaddpi  10893  dmmulpi  10894  smndex1bas  18999  restcldi  23367  cmpsublem  23593  ustuqtop5  24439  tgioo  24990  cphsscph  25447  mdbr3  32686  mdbr4  32687  ssmd1  32700  xrge00  33365  esumpfinvallem  34495  measxun2  34632  eulerpartgbij  34794  reprfz1  35043  tr0elw  37036  tr0el  37037  bj-ismooredr2  37793  bndss  38478  redundss3  39402  dfrcl2  44441  isotone2  44816  wfac8prim  45752  restuni4  45880  fourierdlem93  46954  sge0resplit  47161  mbfresmf  47494