Theorem dfss 3931

Description: Variant of subclass definition df-ss 3930. (Contributed by NM, 21-Jun-1993.)

Assertion

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

Proof of Theorem dfss

Step	Hyp	Ref	Expression
1		df-ss 3930	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2		eqcom 2738	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 ↔ 𝐴 = (𝐴 ∩ 𝐵))
3	1, 2	bitri 274	1 ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 = (𝐴 ∩ 𝐵))

Syntax hints:   ↔ wb 205   = wceq 1541   ∩ cin 3912   ⊆ wss 3913

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723  df-ss 3930

This theorem is referenced by:  dfss2  3933  dfss2OLD  3934  iinrab2  5035  wefrc  5632  cnvcnv  6149  ordtri2or3  6422  onelini  6440  funimass1  6588  sbthlem5  9038  dmaddpi  10835  dmmulpi  10836  smndex1bas  18730  restcldi  22561  cmpsublem  22787  ustuqtop5  23634  tgioo  24196  cphsscph  24652  mdbr3  31302  mdbr4  31303  ssmd1  31316  xrge00  31947  esumpfinvallem  32762  measxun2  32898  eulerpartgbij  33061  reprfz1  33326  bj-ismooredr2  35654  bndss  36318  redundss3  37163  dfrcl2  42068  isotone2  42443  restuni4  43453  fourierdlem93  44560  sge0resplit  44767  mbfresmf  45100