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 1537   ∩ cin 3935   ⊆ wss 3936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2793

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

This theorem is referenced by:  dfss2  3955  iinrab2  4992  wefrc  5549  cnvcnv  6049  ordtri2or3  6288  onelini  6302  funimass1  6436  sbthlem5  8631  dmaddpi  10312  dmmulpi  10313  smndex1bas  18071  restcldi  21781  cmpsublem  22007  ustuqtop5  22854  tgioo  23404  cphsscph  23854  mdbr3  30074  mdbr4  30075  ssmd1  30088  xrge00  30673  esumpfinvallem  31333  measxun2  31469  eulerpartgbij  31630  reprfz1  31895  bj-ismooredr2  34405  bndss  35079  redundss3  35878  dfrcl2  40039  isotone2  40419  restuni4  41407  fourierdlem93  42504  sge0resplit  42708  mbfresmf  43036