Theorem dfss 3899

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

Assertion

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

Proof of Theorem dfss

Step	Hyp	Ref	Expression
1		df-ss 3898	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2		eqcom 2805	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 ↔ 𝐴 = (𝐴 ∩ 𝐵))
3	1, 2	bitri 278	1 ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 = (𝐴 ∩ 𝐵))

Syntax hints:   ↔ wb 209   = wceq 1538   ∩ cin 3880   ⊆ wss 3881

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 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-ss 3898

This theorem is referenced by:  dfss2  3901  dfss2OLD  3902  iinrab2  4955  wefrc  5513  cnvcnv  6016  ordtri2or3  6256  onelini  6270  funimass1  6406  sbthlem5  8615  dmaddpi  10301  dmmulpi  10302  smndex1bas  18063  restcldi  21778  cmpsublem  22004  ustuqtop5  22851  tgioo  23401  cphsscph  23855  mdbr3  30080  mdbr4  30081  ssmd1  30094  xrge00  30720  esumpfinvallem  31443  measxun2  31579  eulerpartgbij  31740  reprfz1  32005  bj-ismooredr2  34525  bndss  35224  redundss3  36023  dfrcl2  40375  isotone2  40752  restuni4  41756  fourierdlem93  42841  sge0resplit  43045  mbfresmf  43373