Theorem dfss 3953

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

Assertion

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

Proof of Theorem dfss

Step	Hyp	Ref	Expression
1		df-ss 3952	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2		eqcom 2828	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 ↔ 𝐴 = (𝐴 ∩ 𝐵))
3	1, 2	bitri 277	1 ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 = (𝐴 ∩ 𝐵))

Syntax hints:   ↔ wb 208   = wceq 1533   ∩ cin 3935   ⊆ wss 3936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814  df-ss 3952

This theorem is referenced by:  dfss2  3955  iinrab2  4985  wefrc  5544  cnvcnv  6044  ordtri2or3  6283  onelini  6297  funimass1  6431  sbthlem5  8625  dmaddpi  10306  dmmulpi  10307  smndex1bas  18065  restcldi  21775  cmpsublem  22001  ustuqtop5  22848  tgioo  23398  cphsscph  23848  mdbr3  30068  mdbr4  30069  ssmd1  30082  xrge00  30668  esumpfinvallem  31328  measxun2  31464  eulerpartgbij  31625  reprfz1  31890  bj-ismooredr2  34396  bndss  35058  redundss3  35857  dfrcl2  40012  isotone2  40392  restuni4  41380  fourierdlem93  42477  sge0resplit  42681  mbfresmf  43009