Theorem dfss 3589

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

Assertion

Ref	Expression
dfss	|- ( A C_ B <-> A = ( A i^i B ) )

Proof of Theorem dfss

Step	Hyp	Ref	Expression
1		df-ss 3588	. 2 |- ( A C_ B <-> ( A i^i B ) = A )
2		eqcom 2629	. 2 |- ( ( A i^i B ) = A <-> A = ( A i^i B ) )
3	1, 2	bitri 264	1 |- ( A C_ B <-> A = ( A i^i B ) )

Syntax hints:   <-> wb 196   = wceq 1483   i^i cin 3573   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-ss 3588

This theorem is referenced by:  dfss2  3591  iinrab2  4583  wefrc  5108  cnvcnv  5586  cnvcnvOLD  5587  ordtri2or3  5824  onelini  5839  funimass1  5971  sbthlem5  8074  dmaddpi  9712  dmmulpi  9713  restcldi  20977  cmpsublem  21202  ustuqtop5  22049  tgioo  22599  mdbr3  29156  mdbr4  29157  ssmd1  29170  xrge00  29686  esumpfinvallem  30136  measxun2  30273  eulerpartgbij  30434  reprfz1  30702  bndss  33585  dfrcl2  37966  isotone2  38347  restuni4  39304  fourierdlem93  40416  sge0resplit  40623  mbfresmf  40948