Definition df-ss 3485

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For example, { 1 , 2 } C_ { 1 , 2 , 3 } (ex-ss 24813). Note that A C_ A (proved in ssid 3518). Contrast this relationship with the relationship A C. B (as will be defined in df-pss 3487). For a more traditional definition, but requiring a dummy variable, see dfss2 3488. Other possible definitions are given by dfss3 3489, dfss4 3727, sspss 3598, ssequn1 3669, ssequn2 3672, sseqin2 3712, and ssdif0 3880. (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 3471	. 2 wff A C_ B
4	1, 2	cin 3470	. . 3 class ( A i^i B )
5	4, 1	wceq 1374	. 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  3486  dfss1  3698  inabs  3724  nssinpss  3725  dfrab3ss  3771  disjssun  3879  riinn0  4395  rintn0  4411  ssex  4586  op1stb  4712  ordtri3or  4905  ssdmres  5288  resima2  5300  xpssres  5301  dmressnsn  5305  fnimaeq0  5695  f0rn0  5763  fnreseql  5984  sorpssin  6565  curry1  6867  curry2  6870  tpostpos2  6968  tz7.44-2  7065  tz7.44-3  7066  frfnom  7092  ecinxp  7378  infssuni  7802  elfiun  7881  marypha1lem  7884  unxpwdom  8006  cdainf  8563  ackbij1lem16  8606  fin23lem26  8696  isf34lem7  8750  isf34lem6  8751  fpwwe2lem11  9009  fpwwe2lem13  9011  fpwwe2  9012  uzin  11105  iooval2  11553  limsupgle  13251  limsupgre  13255  bitsinv1  13942  bitsres  13973  bitsuz  13974  2prm  14083  dfphi2  14154  ressbas2  14537  ressinbas  14542  ressress  14543  restid2  14677  resscatc  15281  pmtrmvd  16272  dprdz  16862  dprdcntz2  16871  lmhmlsp  17473  lspdisj2  17551  ressmplbas2  17883  difopn  19296  mretopd  19354  restcld  19434  restopnb  19437  restfpw  19441  neitr  19442  cnrest2  19548  paste  19556  isnrm2  19620  1stccnp  19724  restnlly  19744  lly1stc  19758  kgeni  19768  kgencn3  19789  ptbasfi  19812  hausdiag  19876  qtopval2  19927  qtoprest  19948  filcon  20114  trfil2  20118  trfg  20122  uzrest  20128  trufil  20141  ufileu  20150  fclscf  20256  flimfnfcls  20259  tsmsresOLD  20375  tsmsres  20376  trust  20462  restutopopn  20471  metustfbasOLD  20798  metustfbas  20799  restmetu  20820  xrtgioo  21041  xrsmopn  21047  clsocv  21420  cmetss  21483  ovoliunlem1  21643  difmbl  21683  voliunlem1  21690  volsup2  21744  i1fima  21815  i1fima2  21816  i1fd  21818  itg1addlem5  21837  itg1climres  21851  dvmptid  22090  dvmptc  22091  dvlipcn  22125  dvlip2  22126  dvcnvrelem1  22148  dvcvx  22151  taylthlem1  22497  taylthlem2  22498  psercn  22550  pige3  22638  dvlog  22755  dvcxp1  22839  ppiprm  23148  chtprm  23150  eupares  24639  chm1i  26038  dmdsl3  26898  atssma  26961  dmdbr6ati  27006  imadifxp  27119  fnresin  27131  sspreima  27145  df1stres  27182  df2ndres  27183  xrge0base  27323  xrge00  27324  xrge0slmod  27485  esumnul  27687  esumsn  27700  eulerpartlemgs2  27947  probmeasb  27997  ballotlemfp1  28058  signstres  28160  cvmscld  28346  cvmliftmolem1  28354  dfon2lem4  28783  dfrdg2  28793  sspred  28817  nodense  29014  fvline2  29361  mblfinlem3  29619  mblfinlem4  29620  ftc1anclem6  29661  areacirclem1  29673  topbnd  29708  opnbnd  29709  neibastop1  29769  subspopn  29837  ssbnd  29876  heiborlem3  29901  elrfi  30219  setindtr  30561  fnwe2lem2  30592  lmhmlnmsplit  30628  proot1hash  30756  fgraphopab  30766  fouriersw  31489  fnresfnco  31635  resisresindm  31731  bnj1322  32837  lcvexchlem3  33710  dihglblem5aN  35966