Definition df-ss 3475

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For example, { 1 , 2 } C_ { 1 , 2 , 3 } (ex-ss 25126). Note that A C_ A (proved in ssid 3508). Contrast this relationship with the relationship A C. B (as will be defined in df-pss 3477). For a more traditional definition, but requiring a dummy variable, see dfss2 3478. Other possible definitions are given by dfss3 3479, dfss4 3717, sspss 3588, ssequn1 3659, ssequn2 3662, sseqin2 3702, and ssdif0 3871. (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 3461	. 2 wff A C_ B
4	1, 2	cin 3460	. . 3 class ( A i^i B )
5	4, 1	wceq 1383	. 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  3476  dfss1  3688  inabs  3714  nssinpss  3715  dfrab3ss  3761  disjssun  3870  riinn0  4390  rintn0  4406  ssex  4581  op1stb  4707  ordtri3or  4900  ssdmres  5285  resima2  5297  xpssres  5298  dmressnsn  5302  fnimaeq0  5692  f0rn0  5760  fnreseql  5982  sorpssin  6573  curry1  6877  curry2  6880  tpostpos2  6978  tz7.44-2  7075  tz7.44-3  7076  frfnom  7102  ecinxp  7388  infssuni  7813  elfiun  7892  marypha1lem  7895  unxpwdom  8018  cdainf  8575  ackbij1lem16  8618  fin23lem26  8708  isf34lem7  8762  isf34lem6  8763  fpwwe2lem11  9021  fpwwe2lem13  9023  fpwwe2  9024  uzin  11124  iooval2  11573  limsupgle  13282  limsupgre  13286  bitsinv1  14074  bitsres  14105  bitsuz  14106  2prm  14215  dfphi2  14286  ressbas2  14670  ressinbas  14675  ressress  14676  restid2  14810  resscatc  15411  pmtrmvd  16460  dprdz  17056  dprdcntz2  17065  lmhmlsp  17674  lspdisj2  17752  ressmplbas2  18096  difopn  19513  mretopd  19571  restcld  19651  restopnb  19654  restfpw  19658  neitr  19659  cnrest2  19765  paste  19773  isnrm2  19837  1stccnp  19941  restnlly  19961  lly1stc  19975  kgeni  20016  kgencn3  20037  ptbasfi  20060  hausdiag  20124  qtopval2  20175  qtoprest  20196  filcon  20362  trfil2  20366  trfg  20370  uzrest  20376  trufil  20389  ufileu  20398  fclscf  20504  flimfnfcls  20507  tsmsresOLD  20623  tsmsres  20624  trust  20710  restutopopn  20719  metustfbasOLD  21046  metustfbas  21047  restmetu  21068  xrtgioo  21289  xrsmopn  21295  clsocv  21668  cmetss  21731  ovoliunlem1  21891  difmbl  21931  voliunlem1  21938  volsup2  21992  i1fima  22063  i1fima2  22064  i1fd  22066  itg1addlem5  22085  itg1climres  22099  dvmptid  22338  dvmptc  22339  dvlipcn  22373  dvlip2  22374  dvcnvrelem1  22396  dvcvx  22399  taylthlem1  22746  taylthlem2  22747  psercn  22799  pige3  22888  dvlog  23010  dvcxp1  23094  ppiprm  23403  chtprm  23405  eupares  24953  chm1i  26352  dmdsl3  27212  atssma  27275  dmdbr6ati  27320  imadifxp  27436  fnresin  27448  sspreima  27463  df1stres  27500  df2ndres  27501  xrge0base  27651  xrge00  27652  xrge0slmod  27812  esumnul  28037  esumsn  28050  eulerpartlemgs2  28297  probmeasb  28347  ballotlemfp1  28408  signstres  28510  cvmscld  28696  cvmliftmolem1  28704  mrsubvrs  28860  elmsta  28886  dfon2lem4  29194  dfrdg2  29204  sspred  29228  nodense  29425  fvline2  29772  mblfinlem3  30029  mblfinlem4  30030  ftc1anclem6  30071  areacirclem1  30083  topbnd  30118  opnbnd  30119  neibastop1  30153  subspopn  30221  ssbnd  30260  heiborlem3  30285  elrfi  30602  setindtr  30942  fnwe2lem2  30973  lmhmlnmsplit  31009  proot1hash  31136  fgraphopab  31146  fouriersw  31968  fnresfnco  32165  resisresindm  32259  ressval3d  32509  lidlbas  32556  bnj1322  33749  lcvexchlem3  34636  dihglblem5aN  36894