Theorem dfss 3945

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

Assertion

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

Proof of Theorem dfss

Step	Hyp	Ref	Expression
1		dfss2 3944	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2		eqcom 2742	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 ↔ 𝐴 = (𝐴 ∩ 𝐵))
3	1, 2	bitri 275	1 ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 = (𝐴 ∩ 𝐵))

Syntax hints:   ↔ wb 206   = wceq 1540   ∩ cin 3925   ⊆ wss 3926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-in 3933  df-ss 3943

This theorem is referenced by:  iinrab2  5046  wefrc  5648  cnvcnv  6181  ordtri2or3  6453  onelini  6471  funimass1  6617  sbthlem5  9099  dmaddpi  10902  dmmulpi  10903  smndex1bas  18882  restcldi  23109  cmpsublem  23335  ustuqtop5  24182  tgioo  24733  cphsscph  25201  mdbr3  32224  mdbr4  32225  ssmd1  32238  xrge00  32953  esumpfinvallem  34051  measxun2  34187  eulerpartgbij  34350  reprfz1  34602  bj-ismooredr2  37074  bndss  37756  redundss3  38592  dfrcl2  43645  isotone2  44020  wfac8prim  44975  restuni4  45093  fourierdlem93  46176  sge0resplit  46383  mbfresmf  46716