Definition df-ss 3588

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For example, { 1 , 2 } C_ { 1 , 2 , 3 } (ex-ss 27284). Note that A C_ A (proved in ssid 3624). Contrast this relationship with the relationship A C. B (as will be defined in df-pss 3590). For a more traditional definition, but requiring a dummy variable, see dfss2 3591. Other possible definitions are given by dfss3 3592, dfss4 3858, sspss 3706, ssequn1 3783, ssequn2 3786, sseqin2 3817, and ssdif0 3942. (Contributed by NM, 27-Apr-1994.)

Assertion

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

Detailed syntax breakdown of Definition df-ss

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	wss 3574	. 2 wff A C_ B
4	1, 2	cin 3573	. . 3 class ( A i^i B )
5	4, 1	wceq 1483	. 2 wff ( A i^i B ) = A
6	3, 5	wb 196	1 wff ( A C_ B <-> ( A i^i B ) = A )

This definition is referenced by:  dfss  3589  sseqin2  3817  dfss1OLD  3818  inabs  3855  nssinpss  3856  dfrab3ss  3905  disjssun  4036  riinn0  4595  ssex  4802  op1stb  4940  ssdmres  5420  resima2OLD  5433  dmressnsn  5438  sspred  5688  ordtri3or  5755  fnimaeq0  6013  f0rn0  6090  fnreseql  6327  sorpssin  6945  curry1  7269  curry2  7272  tpostpos2  7373  tz7.44-2  7503  tz7.44-3  7504  frfnom  7530  ecinxp  7822  infssuni  8257  elfiun  8336  marypha1lem  8339  unxpwdom  8494  cdainf  9014  ackbij1lem16  9057  fin23lem26  9147  isf34lem7  9201  isf34lem6  9202  fpwwe2lem11  9462  fpwwe2lem13  9464  fpwwe2  9465  uzin  11720  iooval2  12208  limsupgle  14208  limsupgre  14212  bitsinv1  15164  bitsres  15195  bitsuz  15196  2prm  15405  dfphi2  15479  ressbas2  15931  ressinbas  15936  ressval3d  15937  ressress  15938  restid2  16091  resscatc  16755  pmtrmvd  17876  dprdz  18429  dprdcntz2  18437  lmhmlsp  19049  lspdisj2  19127  ressmplbas2  19455  difopn  20838  mretopd  20896  restcld  20976  restopnb  20979  restfpw  20983  neitr  20984  cnrest2  21090  paste  21098  isnrm2  21162  1stccnp  21265  restnlly  21285  lly1stc  21299  kgeni  21340  kgencn3  21361  ptbasfi  21384  hausdiag  21448  qtopval2  21499  qtoprest  21520  trfil2  21691  trfg  21695  uzrest  21701  trufil  21714  ufileu  21723  fclscf  21829  flimfnfcls  21832  tsmsres  21947  trust  22033  restutopopn  22042  metustfbas  22362  restmetu  22375  xrtgioo  22609  xrsmopn  22615  clsocv  23049  cmetss  23113  ovoliunlem1  23270  difmbl  23311  voliunlem1  23318  volsup2  23373  i1fima  23445  i1fima2  23446  i1fd  23448  itg1addlem5  23467  itg1climres  23481  dvmptid  23720  dvmptc  23721  dvlipcn  23757  dvlip2  23758  dvcnvrelem1  23780  dvcvx  23783  taylthlem1  24127  taylthlem2  24128  psercn  24180  pige3  24269  dvlog  24397  dvcxp1  24481  ppiprm  24877  chtprm  24879  chm1i  28315  dmdsl3  29174  atssma  29237  dmdbr6ati  29282  imadifxp  29414  fnresin  29430  sspreima  29447  df1stres  29481  df2ndres  29482  xrge0base  29685  xrge00  29686  xrge0slmod  29844  esumnul  30110  esumsnf  30126  baselcarsg  30368  difelcarsg  30372  eulerpartlemgs2  30442  probmeasb  30492  ballotlemfp1  30553  signstres  30652  ftc2re  30676  bnj1322  30893  cvmscld  31255  cvmliftmolem1  31263  mrsubvrs  31419  elmsta  31445  dfon2lem4  31691  dfrdg2  31701  nolesgn2ores  31825  nodense  31842  nosupres  31853  nosupbnd2lem1  31861  fvline2  32253  topbnd  32319  opnbnd  32320  neibastop1  32354  bj-disj2r  33013  bj-restsnss2  33037  bj-0int  33055  mblfinlem3  33448  mblfinlem4  33449  ftc1anclem6  33490  areacirclem1  33500  subspopn  33548  ssbnd  33587  heiborlem3  33612  lcvexchlem3  34323  dihglblem5aN  36581  elrfi  37257  setindtr  37591  fnwe2lem2  37621  lmhmlnmsplit  37657  proot1hash  37778  fgraphopab  37788  iunrelexp0  37994  gneispace  38432  uzinico2  39789  limsupval3  39924  limsupvaluz  39940  liminfval5  39997  fouriersw  40448  saliincl  40545  saldifcl2  40546  gsumge0cl  40588  sge0sn  40596  sge0tsms  40597  sge0split  40626  caragenunidm  40722  fnresfnco  41206  lidlbas  41923