Definition df-ss 3430

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For example, { 1 , 2 } C_ { 1 , 2 , 3 } (ex-ss 25933). Note that A C_ A (proved in ssid 3463). Contrast this relationship with the relationship A C. B (as will be defined in df-pss 3432). For a more traditional definition, but requiring a dummy variable, see dfss2 3433. Other possible definitions are given by dfss3 3434, dfss4 3689, sspss 3544, ssequn1 3616, ssequn2 3619, sseqin2 3663, and ssdif0 3835. (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 3416	. 2 wff A C_ B
4	1, 2	cin 3415	. . 3 class ( A i^i B )
5	4, 1	wceq 1455	. 2 wff ( A i^i B ) = A
6	3, 5	wb 189	1 wff ( A C_ B <-> ( A i^i B ) = A )

This definition is referenced by:  dfss  3431  dfss1  3649  inabs  3686  nssinpss  3687  dfrab3ss  3733  disjssun  3834  riinn0  4367  rintn0  4388  ssex  4563  op1stb  4689  ssdmres  5148  resima2  5160  xpssres  5161  dmressnsn  5165  sspred  5411  ordtri3or  5478  fnimaeq0  5723  f0rn0  5795  fnreseql  6020  sorpssin  6611  curry1  6920  curry2  6923  tpostpos2  7025  tz7.44-2  7156  tz7.44-3  7157  frfnom  7183  ecinxp  7469  infssuni  7896  elfiun  7975  marypha1lem  7978  unxpwdom  8135  cdainf  8653  ackbij1lem16  8696  fin23lem26  8786  isf34lem7  8840  isf34lem6  8841  fpwwe2lem11  9096  fpwwe2lem13  9098  fpwwe2  9099  uzin  11225  iooval2  11703  limsupgle  13590  limsupgre  13597  limsupgreOLD  13598  bitsinv1  14471  bitsres  14502  bitsuz  14503  2prm  14695  dfphi2  14777  ressbas2  15235  ressinbas  15240  ressval3d  15241  ressress  15242  restid2  15384  resscatc  16055  pmtrmvd  17152  dprdz  17718  dprdcntz2  17726  lmhmlsp  18327  lspdisj2  18405  ressmplbas2  18734  difopn  20104  mretopd  20163  restcld  20243  restopnb  20246  restfpw  20250  neitr  20251  cnrest2  20357  paste  20365  isnrm2  20429  1stccnp  20532  restnlly  20552  lly1stc  20566  kgeni  20607  kgencn3  20628  ptbasfi  20651  hausdiag  20715  qtopval2  20766  qtoprest  20787  filcon  20953  trfil2  20957  trfg  20961  uzrest  20967  trufil  20980  ufileu  20989  fclscf  21095  flimfnfcls  21098  tsmsres  21213  trust  21299  restutopopn  21308  metustfbas  21627  restmetu  21640  xrtgioo  21879  xrsmopn  21885  clsocv  22276  cmetss  22339  ovoliunlem1  22510  difmbl  22552  voliunlem1  22559  volsup2  22619  i1fima  22692  i1fima2  22693  i1fd  22695  itg1addlem5  22714  itg1climres  22728  dvmptid  22967  dvmptc  22968  dvlipcn  23002  dvlip2  23003  dvcnvrelem1  23025  dvcvx  23028  taylthlem1  23384  taylthlem2  23385  psercn  23437  pige3  23528  dvlog  23652  dvcxp1  23736  ppiprm  24134  chtprm  24136  eupares  25759  chm1i  27165  dmdsl3  28024  atssma  28087  dmdbr6ati  28132  imadifxp  28265  fnresin  28281  sspreima  28299  df1stres  28336  df2ndres  28337  xrge0base  28499  xrge00  28500  xrge0slmod  28658  esumnul  28920  esumsnf  28936  baselcarsg  29188  difelcarsg  29192  eulerpartlemgs2  29263  probmeasb  29313  ballotlemfp1  29374  signstres  29514  bnj1322  29684  cvmscld  30046  cvmliftmolem1  30054  mrsubvrs  30210  elmsta  30236  dfon2lem4  30482  dfrdg2  30492  nodense  30628  fvline2  30963  topbnd  31030  opnbnd  31031  neibastop1  31065  mblfinlem3  32025  mblfinlem4  32026  ftc1anclem6  32068  areacirclem1  32078  subspopn  32127  ssbnd  32166  heiborlem3  32191  lcvexchlem3  32648  dihglblem5aN  34906  elrfi  35582  setindtr  35925  fnwe2lem2  35955  lmhmlnmsplit  35991  proot1hash  36123  fgraphopab  36133  iunrelexp0  36340  fouriersw  38196  saliincl  38287  saldifcl2  38288  gsumge0cl  38316  sge0sn  38324  sge0tsms  38325  sge0split  38354  caragenunidm  38437  fnresfnco  38762  resisresindm  39147  lidlbas  40292