Theorem dfss 3918

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

Assertion

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

Proof of Theorem dfss

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

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

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 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-in 3906  df-ss 3916

This theorem is used by:  iinrab2  5028  wefrc  5645  cnvcnv  6183  ordtri2or3  6458  onelini  6475  funimass1  6614  sbthlem5  9094  dmaddpi  10956  dmmulpi  10957  smndex1bas  19085  restcldi  23471  cmpsublem  23697  ustuqtop5  24544  tgioo  25095  cphsscph  25552  mdbr3  32881  mdbr4  32882  ssmd1  32895  xrge00  33557  esumpfinvallem  34688  measxun2  34825  eulerpartgbij  34987  reprfz1  35236  tr0elw  37242  tr0el  37243  bj-ismooredr2  37999  bndss  38688  redundss3  39612  dfrcl2  44633  isotone2  45008  wfac8prim  45944  restuni4  46079  fourierdlem93  47153  sge0resplit  47360  mbfresmf  47693