Definition df-ss 3294

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For example, { 1 , 2 } C_ { 1 , 2 , 3 } (ex-ss 21688). Note that A C_ A (proved in ssid 3327). Contrast this relationship with the relationship A C. B (as will be defined in df-pss 3296). For a more traditional definition, but requiring a dummy variable, see dfss2 3297. Other possible definitions are given by dfss3 3298, dfss4 3535, sspss 3406, ssequn1 3477, ssequn2 3480, sseqin2 3520, and ssdif0 3646. (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 3280	. 2 wff A C_ B
4	1, 2	cin 3279	. . 3 class ( A i^i B )
5	4, 1	wceq 1649	. 2 wff ( A i^i B ) = A
6	3, 5	wb 177	1 wff ( A C_ B <-> ( A i^i B ) = A )

This definition is referenced by:  dfss  3295  dfss1  3505  inabs  3532  nssinpss  3533  dfrab3ss  3579  disjssun  3645  riinn0  4125  rintn0  4141  ssex  4307  ordtri3or  4573  op1stb  4717  ssdmres  5127  resima2  5138  xpssres  5139  fnimaeq0  5525  fnreseql  5799  curry1  6397  curry2  6400  tpostpos2  6459  sorpssin  6489  tz7.44-2  6624  tz7.44-3  6625  frfnom  6651  ecinxp  6938  elfiun  7393  marypha1lem  7396  unxpwdom  7513  cdainf  8028  ackbij1lem16  8071  fin23lem26  8161  isf34lem7  8215  isf34lem6  8216  fpwwe2lem11  8471  fpwwe2lem13  8473  fpwwe2  8474  uzin  10474  iooval2  10905  limsupgle  12226  limsupgre  12230  bitsinv1  12909  bitsres  12940  bitsuz  12941  2prm  13050  dfphi2  13118  ressbas2  13475  ressinbas  13480  ressress  13481  restid2  13613  resscatc  14215  dprdz  15543  dprdcntz2  15551  lmhmlsp  16080  lspdisj2  16154  ressmplbas2  16473  difopn  17053  mretopd  17111  restcld  17190  restopnb  17193  restfpw  17197  neitr  17198  cnrest2  17304  paste  17312  isnrm2  17376  1stccnp  17478  restnlly  17498  lly1stc  17512  kgeni  17522  kgencn3  17543  ptbasfi  17566  hausdiag  17630  qtopval2  17681  qtoprest  17702  filcon  17868  trfil2  17872  trfg  17876  uzrest  17882  trufil  17895  ufileu  17904  fclscf  18010  flimfnfcls  18013  tsmsres  18126  trust  18212  restutopopn  18221  metustfbasOLD  18548  metustfbas  18549  restmetu  18570  xrtgioo  18790  xrsmopn  18796  clsocv  19157  cmetss  19220  ovoliunlem1  19351  difmbl  19390  voliunlem1  19397  volsup2  19450  i1fima  19523  i1fima2  19524  i1fd  19526  itg1addlem5  19545  itg1climres  19559  dvmptid  19796  dvmptc  19797  dvlipcn  19831  dvlip2  19832  dvcnvrelem1  19854  dvcvx  19857  taylthlem1  20242  taylthlem2  20243  psercn  20295  pige3  20378  dvlog  20495  dvcxp1  20579  ppiprm  20887  chtprm  20889  eupares  21650  chm1i  22911  dmdsl3  23771  atssma  23834  dmdbr6ati  23879  imadifxp  23991  sspreima  24010  df1stres  24044  df2ndres  24045  xrge0base  24160  xrge00  24161  esumnul  24396  esumsn  24409  probmeasb  24641  ballotlemfp1  24702  cvmscld  24913  cvmliftmolem1  24921  dfon2lem4  25356  dfrdg2  25366  sspred  25388  nodense  25557  fvline2  25984  mblfinlem2  26144  mblfinlem3  26145  dvreasin  26179  areacirclem2  26181  areacirclem3  26182  topbnd  26217  opnbnd  26218  neibastop1  26278  subspopn  26348  ssbnd  26387  heiborlem3  26412  elrfi  26638  setindtr  26985  fnwe2lem2  27016  lmhmlnmsplit  27053  pmtrmvd  27266  proot1hash  27387  fgraphopab  27397  dmressnsn  27852  fnresfnco  27857  resisresindm  27957  bnj1322  28900  lcvexchlem3  29519  dihglblem5aN  31775