Definition df-ss 3456

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For example, { 1 , 2 } C_ { 1 , 2 , 3 } (ex-ss 25722). Note that A C_ A (proved in ssid 3489). Contrast this relationship with the relationship A C. B (as will be defined in df-pss 3458). For a more traditional definition, but requiring a dummy variable, see dfss2 3459. Other possible definitions are given by dfss3 3460, dfss4 3713, sspss 3570, ssequn1 3642, ssequn2 3645, sseqin2 3687, and ssdif0 3857. (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 3442	. 2 wff A C_ B
4	1, 2	cin 3441	. . 3 class ( A i^i B )
5	4, 1	wceq 1437	. 2 wff ( A i^i B ) = A
6	3, 5	wb 187	1 wff ( A C_ B <-> ( A i^i B ) = A )

This definition is referenced by:  dfss  3457  dfss1  3673  inabs  3710  nssinpss  3711  dfrab3ss  3757  disjssun  3856  riinn0  4377  rintn0  4396  ssex  4569  op1stb  4692  ssdmres  5146  resima2  5158  xpssres  5159  dmressnsn  5163  sspred  5407  ordtri3or  5474  fnimaeq0  5715  f0rn0  5785  fnreseql  6007  sorpssin  6593  curry1  6899  curry2  6902  tpostpos2  7002  tz7.44-2  7133  tz7.44-3  7134  frfnom  7160  ecinxp  7446  infssuni  7871  elfiun  7950  marypha1lem  7953  unxpwdom  8104  cdainf  8620  ackbij1lem16  8663  fin23lem26  8753  isf34lem7  8807  isf34lem6  8808  fpwwe2lem11  9064  fpwwe2lem13  9066  fpwwe2  9067  uzin  11191  iooval2  11669  limsupgle  13513  limsupgre  13520  limsupgreOLD  13521  bitsinv1  14390  bitsres  14421  bitsuz  14422  2prm  14611  dfphi2  14691  ressbas2  15142  ressinbas  15147  ressval3d  15148  ressress  15149  restid2  15288  resscatc  15951  pmtrmvd  17048  dprdz  17598  dprdcntz2  17606  lmhmlsp  18207  lspdisj2  18285  ressmplbas2  18614  difopn  19980  mretopd  20039  restcld  20119  restopnb  20122  restfpw  20126  neitr  20127  cnrest2  20233  paste  20241  isnrm2  20305  1stccnp  20408  restnlly  20428  lly1stc  20442  kgeni  20483  kgencn3  20504  ptbasfi  20527  hausdiag  20591  qtopval2  20642  qtoprest  20663  filcon  20829  trfil2  20833  trfg  20837  uzrest  20843  trufil  20856  ufileu  20865  fclscf  20971  flimfnfcls  20974  tsmsres  21089  trust  21175  restutopopn  21184  metustfbas  21503  restmetu  21516  xrtgioo  21735  xrsmopn  21741  clsocv  22114  cmetss  22177  ovoliunlem1  22333  difmbl  22373  voliunlem1  22380  volsup2  22440  i1fima  22513  i1fima2  22514  i1fd  22516  itg1addlem5  22535  itg1climres  22549  dvmptid  22788  dvmptc  22789  dvlipcn  22823  dvlip2  22824  dvcnvrelem1  22846  dvcvx  22849  taylthlem1  23193  taylthlem2  23194  psercn  23246  pige3  23337  dvlog  23461  dvcxp1  23545  ppiprm  23941  chtprm  23943  eupares  25548  chm1i  26944  dmdsl3  27803  atssma  27866  dmdbr6ati  27911  imadifxp  28051  fnresin  28068  sspreima  28086  df1stres  28124  df2ndres  28125  xrge0base  28284  xrge00  28285  xrge0slmod  28446  esumnul  28708  esumsnf  28724  baselcarsg  28967  difelcarsg  28971  eulerpartlemgs2  29039  probmeasb  29089  ballotlemfp1  29150  signstres  29252  bnj1322  29422  cvmscld  29784  cvmliftmolem1  29792  mrsubvrs  29948  elmsta  29974  dfon2lem4  30219  dfrdg2  30229  nodense  30363  fvline2  30698  topbnd  30765  opnbnd  30766  neibastop1  30800  mblfinlem3  31682  mblfinlem4  31683  ftc1anclem6  31725  areacirclem1  31735  subspopn  31784  ssbnd  31823  heiborlem3  31848  lcvexchlem3  32310  dihglblem5aN  34568  elrfi  35244  setindtr  35584  fnwe2lem2  35614  lmhmlnmsplit  35650  proot1hash  35775  fgraphopab  35785  iunrelexp0  35932  fouriersw  37662  saliincl  37732  saldifcl2  37733  gsumge0cl  37746  sge0sn  37754  sge0tsms  37755  sge0split  37784  caragenunidm  37837  fnresfnco  38017  resisresindm  38381  lidlbas  38680