Definition df-ss 3403

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For example, { 1 , 2 } C_ { 1 , 2 , 3 } (ex-ss 25269). Note that A C_ A (proved in ssid 3436). Contrast this relationship with the relationship A C. B (as will be defined in df-pss 3405). For a more traditional definition, but requiring a dummy variable, see dfss2 3406. Other possible definitions are given by dfss3 3407, dfss4 3657, sspss 3517, ssequn1 3588, ssequn2 3591, sseqin2 3631, and ssdif0 3801. (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 3389	. 2 wff A C_ B
4	1, 2	cin 3388	. . 3 class ( A i^i B )
5	4, 1	wceq 1399	. 2 wff ( A i^i B ) = A
6	3, 5	wb 184	1 wff ( A C_ B <-> ( A i^i B ) = A )

This definition is referenced by:  dfss  3404  dfss1  3617  inabs  3654  nssinpss  3655  dfrab3ss  3701  disjssun  3800  riinn0  4318  rintn0  4337  ssex  4509  op1stb  4632  ordtri3or  4824  ssdmres  5207  resima2  5219  xpssres  5220  dmressnsn  5224  fnimaeq0  5610  f0rn0  5678  fnreseql  5899  sorpssin  6487  curry1  6791  curry2  6794  tpostpos2  6894  tz7.44-2  6991  tz7.44-3  6992  frfnom  7018  ecinxp  7304  infssuni  7726  elfiun  7805  marypha1lem  7808  unxpwdom  7930  cdainf  8485  ackbij1lem16  8528  fin23lem26  8618  isf34lem7  8672  isf34lem6  8673  fpwwe2lem11  8929  fpwwe2lem13  8931  fpwwe2  8932  uzin  11033  iooval2  11483  limsupgle  13302  limsupgre  13306  bitsinv1  14094  bitsres  14125  bitsuz  14126  2prm  14235  dfphi2  14306  ressbas2  14692  ressinbas  14697  ressval3d  14698  ressress  14699  restid2  14838  resscatc  15501  pmtrmvd  16598  dprdz  17190  dprdcntz2  17199  lmhmlsp  17808  lspdisj2  17886  ressmplbas2  18230  difopn  19620  mretopd  19679  restcld  19759  restopnb  19762  restfpw  19766  neitr  19767  cnrest2  19873  paste  19881  isnrm2  19945  1stccnp  20048  restnlly  20068  lly1stc  20082  kgeni  20123  kgencn3  20144  ptbasfi  20167  hausdiag  20231  qtopval2  20282  qtoprest  20303  filcon  20469  trfil2  20473  trfg  20477  uzrest  20483  trufil  20496  ufileu  20505  fclscf  20611  flimfnfcls  20614  tsmsresOLD  20730  tsmsres  20731  trust  20817  restutopopn  20826  metustfbasOLD  21153  metustfbas  21154  restmetu  21175  xrtgioo  21396  xrsmopn  21402  clsocv  21775  cmetss  21838  ovoliunlem1  21998  difmbl  22038  voliunlem1  22045  volsup2  22099  i1fima  22170  i1fima2  22171  i1fd  22173  itg1addlem5  22192  itg1climres  22206  dvmptid  22445  dvmptc  22446  dvlipcn  22480  dvlip2  22481  dvcnvrelem1  22503  dvcvx  22506  taylthlem1  22853  taylthlem2  22854  psercn  22906  pige3  22995  dvlog  23119  dvcxp1  23203  ppiprm  23542  chtprm  23544  eupares  25096  chm1i  26491  dmdsl3  27350  atssma  27413  dmdbr6ati  27458  imadifxp  27591  fnresin  27608  sspreima  27625  df1stres  27669  df2ndres  27670  xrge0base  27826  xrge00  27827  xrge0slmod  27988  esumnul  28196  esumsnf  28212  baselcarsg  28433  difelcarsg  28437  eulerpartlemgs2  28502  probmeasb  28552  ballotlemfp1  28613  signstres  28715  cvmscld  28907  cvmliftmolem1  28915  mrsubvrs  29071  elmsta  29097  dfon2lem4  29383  dfrdg2  29393  sspred  29417  nodense  29614  fvline2  29949  mblfinlem3  30218  mblfinlem4  30219  ftc1anclem6  30261  areacirclem1  30273  topbnd  30308  opnbnd  30309  neibastop1  30343  subspopn  30411  ssbnd  30450  heiborlem3  30475  elrfi  30792  setindtr  31132  fnwe2lem2  31163  lmhmlnmsplit  31199  proot1hash  31328  fgraphopab  31338  fouriersw  32180  fnresfnco  32377  resisresindm  32626  lidlbas  32929  bnj1322  34228  lcvexchlem3  35174  dihglblem5aN  37432  iunrelexp0  38242