Definition df-ss 3450

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For example, { 1 , 2 } C_ { 1 , 2 , 3 } (ex-ss 25875). Note that A C_ A (proved in ssid 3483). Contrast this relationship with the relationship A C. B (as will be defined in df-pss 3452). For a more traditional definition, but requiring a dummy variable, see dfss2 3453. Other possible definitions are given by dfss3 3454, dfss4 3707, sspss 3564, ssequn1 3636, ssequn2 3639, sseqin2 3681, and ssdif0 3853. (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 3436	. 2 wff A C_ B
4	1, 2	cin 3435	. . 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  3451  dfss1  3667  inabs  3704  nssinpss  3705  dfrab3ss  3751  disjssun  3852  riinn0  4374  rintn0  4393  ssex  4568  op1stb  4691  ssdmres  5145  resima2  5157  xpssres  5158  dmressnsn  5162  sspred  5407  ordtri3or  5474  fnimaeq0  5715  f0rn0  5785  fnreseql  6007  sorpssin  6593  curry1  6899  curry2  6902  tpostpos2  7005  tz7.44-2  7136  tz7.44-3  7137  frfnom  7163  ecinxp  7449  infssuni  7874  elfiun  7953  marypha1lem  7956  unxpwdom  8113  cdainf  8629  ackbij1lem16  8672  fin23lem26  8762  isf34lem7  8816  isf34lem6  8817  fpwwe2lem11  9072  fpwwe2lem13  9074  fpwwe2  9075  uzin  11198  iooval2  11676  limsupgle  13534  limsupgre  13541  limsupgreOLD  13542  bitsinv1  14415  bitsres  14446  bitsuz  14447  2prm  14639  dfphi2  14721  ressbas2  15179  ressinbas  15184  ressval3d  15185  ressress  15186  restid2  15328  resscatc  15999  pmtrmvd  17096  dprdz  17662  dprdcntz2  17670  lmhmlsp  18271  lspdisj2  18349  ressmplbas2  18678  difopn  20047  mretopd  20106  restcld  20186  restopnb  20189  restfpw  20193  neitr  20194  cnrest2  20300  paste  20308  isnrm2  20372  1stccnp  20475  restnlly  20495  lly1stc  20509  kgeni  20550  kgencn3  20571  ptbasfi  20594  hausdiag  20658  qtopval2  20709  qtoprest  20730  filcon  20896  trfil2  20900  trfg  20904  uzrest  20910  trufil  20923  ufileu  20932  fclscf  21038  flimfnfcls  21041  tsmsres  21156  trust  21242  restutopopn  21251  metustfbas  21570  restmetu  21583  xrtgioo  21822  xrsmopn  21828  clsocv  22219  cmetss  22282  ovoliunlem1  22453  difmbl  22494  voliunlem1  22501  volsup2  22561  i1fima  22634  i1fima2  22635  i1fd  22637  itg1addlem5  22656  itg1climres  22670  dvmptid  22909  dvmptc  22910  dvlipcn  22944  dvlip2  22945  dvcnvrelem1  22967  dvcvx  22970  taylthlem1  23326  taylthlem2  23327  psercn  23379  pige3  23470  dvlog  23594  dvcxp1  23678  ppiprm  24076  chtprm  24078  eupares  25701  chm1i  27107  dmdsl3  27966  atssma  28029  dmdbr6ati  28074  imadifxp  28214  fnresin  28230  sspreima  28248  df1stres  28286  df2ndres  28287  xrge0base  28454  xrge00  28455  xrge0slmod  28615  esumnul  28877  esumsnf  28893  baselcarsg  29146  difelcarsg  29150  eulerpartlemgs2  29221  probmeasb  29271  ballotlemfp1  29332  signstres  29472  bnj1322  29642  cvmscld  30004  cvmliftmolem1  30012  mrsubvrs  30168  elmsta  30194  dfon2lem4  30439  dfrdg2  30449  nodense  30583  fvline2  30918  topbnd  30985  opnbnd  30986  neibastop1  31020  mblfinlem3  31943  mblfinlem4  31944  ftc1anclem6  31986  areacirclem1  31996  subspopn  32045  ssbnd  32084  heiborlem3  32109  lcvexchlem3  32571  dihglblem5aN  34829  elrfi  35505  setindtr  35849  fnwe2lem2  35879  lmhmlnmsplit  35915  proot1hash  36047  fgraphopab  36057  iunrelexp0  36264  fouriersw  38035  saliincl  38107  saldifcl2  38108  gsumge0cl  38121  sge0sn  38129  sge0tsms  38130  sge0split  38159  caragenunidm  38237  fnresfnco  38498  resisresindm  38875  lidlbas  39543